1  /-
  2  Copyright (c) 2019 Jeremy Avigad. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Jeremy Avigad, Yury Kudryashov
  5  -/
  6  
  7  import analysis.normed_space.basic tactic.alias
src         └─────────────────────────┘ └──────────┘
  8  
  9  /-!
 10  # Asymptotics
 11  
 12  We introduce these relations:
 13  
 14  * `is_O_with c f g l` : "f is big O of g along l with constant c";
 15  * `is_O f g l` : "f is big O of g along l";
 16  * `is_o f g l` : "f is little o of g along l".
 17  
 18  Here `l` is any filter on the domain of `f` and `g`, which are assumed to be the same. The codomains
 19  of `f` and `g` do not need to be the same; all that is needed that there is a norm associated with
 20  these types, and it is the norm that is compared asymptotically.
 21  
 22  The relation `is_O_with c` is introduced to factor out common algebraic arguments in the proofs of
 23  similar properties of `is_O` and `is_o`. Usually proofs outside of this file should use `is_O`
 24  instead.
 25  
 26  Often the ranges of `f` and `g` will be the real numbers, in which case the norm is the absolute
 27  value. In general, we have
 28  
 29    `is_O f g l ↔ is_O (λ x, ∥f x∥) (λ x, ∥g x∥) l`,
 30  
 31  and similarly for `is_o`. But our setup allows us to use the notions e.g. with functions
 32  to the integers, rationals, complex numbers, or any normed vector space without mentioning the
 33  norm explicitly.
 34  
 35  If `f` and `g` are functions to a normed field like the reals or complex numbers and `g` is always
 36  nonzero, we have
 37  
 38    `is_o f g l ↔ tendsto (λ x, f x / (g x)) l (𝓝 0)`.
 39  
 40  In fact, the right-to-left direction holds without the hypothesis on `g`, and in the other direction
 41  it suffices to assume that `f` is zero wherever `g` is. (This generalization is useful in defining
 42  the Fréchet derivative.)
 43  -/
 44  
 45  open filter set
 46  open_locale topological_space
 47  
 48  namespace asymptotics
 49  
 50  variables {α : Type*} {β : Type*} {E : Type*} {F : Type*} {G : Type*}
 51    {E' : Type*} {F' : Type*} {G' : Type*} {R : Type*} {R' : Type*} {𝕜 : Type*} {𝕜' : Type*}
 52  
 53  variables [has_norm E] [has_norm F] [has_norm G] [normed_group E'] [normed_group F']
id              └──────┘     └──────┘     └──────┘     └──────────┘      └──────────┘
src             └──────┘     └──────┘     └──────┘     └──────────┘      └──────────┘
typ             └──────┘     └──────┘     └──────┘     └──────────┘      └──────────┘
doc             └──────┘     └──────┘     └──────┘     └──────────┘      └──────────┘
 54    [normed_group G'] [normed_ring R] [normed_ring R'] [normed_field 𝕜] [normed_field 𝕜']
id      └──────────┘      └─────────┘     └─────────┘      └──────────┘     └──────────┘
src     └──────────┘      └─────────┘     └─────────┘      └──────────┘     └──────────┘
typ     └──────────┘      └─────────┘     └─────────┘      └──────────┘     └──────────┘
doc     └──────────┘      └─────────┘     └─────────┘      └──────────┘     └──────────┘
 55    {c c' : ℝ} {f : α → E} {g : α → F} {k : α → G} {f' : α → E'} {g' : α → F'} {k' : α → G'}
id             
src            
typ            
 56    {l l' : filter α}
id             └────┘
src            └────┘
typ            └────┘
 57  
 58  section defs
 59  
 60  /-! ### Definitions -/
 61  
 62  /-- This version of the Landau notation `is_O_with C f g l` where `f` and `g` are two functions on
 63  a type `α` and `l` is a filter on `α`, means that eventually for `l`, `∥f∥` is bounded by `C * ∥g∥`.
 64  In other words, `∥f∥ / ∥g∥` is eventually bounded by `C`, modulo division by zero issues that are
 65  avoided by this definition. Probably you want to use `is_O` instead of this relation. -/
 66  def is_O_with (c : ℝ) (f : α → E) (g : α → F) (l : filter α) : Prop :=
id                                                 └────┘ 
src                                                    └────┘
typ                                                └────┘ 
 67  ∀ᶠ x in l, ∥ f x ∥ ≤ c * ∥ g x ∥
id   └┘  └┘            
src  └┘   └┘                  
typ  └┘  └┘            
doc  └┘   └┘  
 68  
 69  /-- The Landau notation `is_O f g l` where `f` and `g` are two functions on a type `α` and `l` is
 70  a filter on `α`, means that eventually for `l`, `∥f∥` is bounded by a constant multiple of `∥g∥`.
 71  In other words, `∥f∥ / ∥g∥` is eventually bounded, modulo division by zero issues that are avoided
 72  by this definition. -/
 73  def is_O (f : α → E) (g : α → F) (l : filter α) : Prop := ∃ c : ℝ, is_O_with c f g l
id                                     └────┘                   └───────┘    
src                                        └────┘                    └───────┘
typ                                    └────┘                   └───────┘    
doc                                                                     └───────┘
 74  
 75  /-- The Landau notation `is_o f g l` where `f` and `g` are two functions on a type `α` and `l` is
 76  a filter on `α`, means that eventually for `l`, `∥f∥` is bounded by an arbitrarily small constant
 77  multiple of `∥g∥`. In other words, `∥f∥ / ∥g∥` tends to `0` along `l`, modulo division by zero
 78  issues that are avoided by this definition. -/
 79  def is_o (f : α → E) (g : α → F) (l : filter α) : Prop := ∀ ⦃c : ℝ⦄, 0 < c → is_O_with c f g l
id                                     └────┘                             └───────┘    
src                                        └────┘                               └───────┘
typ                                    └────┘                             └───────┘    
doc                                                                               └───────┘
 80  
 81  end defs
 82  
 83  /-! ### Conversions -/
 84  
 85  theorem is_O_with.is_O (h : is_O_with c f g l) : is_O f g l := ⟨c, h⟩
id                               └───────┘        └──┘          
src                              └───────┘            └──┘
typ                              └───────┘        └──┘          
doc                              └───────┘            └──┘
 86  
 87  theorem is_o.is_O_with (hgf : is_o f g l) : is_O_with 1 f g l := hgf zero_lt_one
id                                 └──┘       └───────┘         └─┘ └─────────┘
src                                └──┘          └───────┘                └─────────┘
typ                                └──┘       └───────┘         └─┘ └─────────┘
doc                                └──┘          └───────┘
 88  
 89  theorem is_o.is_O (hgf : is_o f g l) : is_O f g l := hgf.is_O_with.is_O
id                            └──┘       └──┘       └─┘└────────┘└───┘
src                           └──┘          └──┘             └────────┘└───┘
typ                           └──┘       └──┘       └─┘└────────┘└───┘
doc                           └──┘          └──┘
 90  
 91  theorem is_O_with.weaken (h : is_O_with c f g' l) (hc : c ≤ c') : is_O_with c' f g' l :=
id                                 └───────┘   └┘           └┘    └───────┘ └┘  └┘ 
src                                └───────┘                          └───────┘
typ                                └───────┘   └┘           └┘    └───────┘ └┘  └┘ 
doc                                └───────┘                           └───────┘
 92  mem_sets_of_superset h $ λ x hx,
id   └──────────────────┘       └┘
src  └──────────────────┘
typ  └──────────────────┘       └┘
 93  calc ∥f x∥ ≤ c * ∥g' x∥ : hx
id              └┘    └┘
src                    
typ             └┘    └┘
 94  ... ≤ _ : mul_le_mul_of_nonneg_right hc (norm_nonneg _)
id             └────────────────────────┘ └┘  └─────────┘
src            └────────────────────────┘     └─────────┘
typ            └────────────────────────┘ └┘  └─────────┘
 95  
 96  theorem is_O_with.exists_pos (h : is_O_with c f g' l) :
id                                     └───────┘   └┘ 
src                                    └───────┘
typ                                    └───────┘   └┘ 
doc                                    └───────┘
 97    ∃ c' (H : 0 < c'), is_O_with c' f g' l :=
id      └┘         └┘  └───────┘ └┘  └┘ 
src                    └───────┘
typ     └┘         └┘  └───────┘ └┘  └┘ 
doc                       └───────┘
 98  ⟨max c 1, lt_of_lt_of_le zero_lt_one (le_max_right c 1), h.weaken $ le_max_left c 1⟩
id    └─┘     └────────────┘ └─────────┘  └──────────┘      └─────┘   └─────────┘ 
src   └─┘      └────────────┘ └─────────┘  └──────────┘        └─────┘   └─────────┘
typ   └─┘     └────────────┘ └─────────┘  └──────────┘      └─────┘   └─────────┘ 
 99  
100  theorem is_O.exists_pos (h : is_O f g' l) : ∃ c (H : 0 < c), is_O_with c f g' l :=
id                                └──┘  └┘                 └───────┘   └┘ 
src                               └──┘                         └───────┘
typ                               └──┘  └┘                 └───────┘   └┘ 
doc                               └──┘                            └───────┘
101  let ⟨c, hc⟩ := h in hc.exists_pos
id   └─┘     └┘           └─────────┘
src                        └─────────┘
typ  └─┘     └┘           └─────────┘
102  
103  theorem is_O_with.exists_nonneg (h : is_O_with c f g' l) :
id                                        └───────┘   └┘ 
src                                       └───────┘
typ                                       └───────┘   └┘ 
doc                                       └───────┘
104    ∃ c' (H : 0 ≤ c'), is_O_with c' f g' l :=
id      └┘         └┘  └───────┘ └┘  └┘ 
src                    └───────┘
typ     └┘         └┘  └───────┘ └┘  └┘ 
doc                       └───────┘
105  let ⟨c, cpos, hc⟩ := h.exists_pos in ⟨c, le_of_lt cpos, hc⟩
id   └─┘    └──┘  └┘     └─────────┘        └──────┘
src                        └─────────┘        └──────┘
typ  └─┘    └──┘  └┘     └─────────┘        └──────┘
106  
107  theorem is_O.exists_nonneg (h : is_O f g' l) :
id                                   └──┘  └┘ 
src                                  └──┘
typ                                  └──┘  └┘ 
doc                                  └──┘
108    ∃ c (H : 0 ≤ c), is_O_with c f g' l :=
id                 └───────┘   └┘ 
src                  └───────┘
typ                └───────┘   └┘ 
doc                     └───────┘
109  let ⟨c, hc⟩ := h in hc.exists_nonneg
id   └─┘     └┘           └────────────┘
src                        └────────────┘
typ  └─┘     └┘           └────────────┘
110  
111  /-! ### Congruence -/
112  
113  theorem is_O_with_congr {c₁ c₂} {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α}
id                                                                    └────┘ 
src                                                                       └────┘
typ                                                                   └────┘ 
114    (hc : c₁ = c₂) (hf : ∀ᶠ x in l, f₁ x = f₂ x) (hg : ∀ᶠ x in l, g₁ x = g₂ x) :
id           └┘  └┘        └┘  └┘  └┘   └┘         └┘  └┘  └┘   └┘ 
src                        └┘   └┘                     └┘   └┘        
typ          └┘  └┘        └┘  └┘  └┘   └┘         └┘  └┘  └┘   └┘ 
doc                         └┘   └┘                      └┘   └┘  
115    is_O_with c₁ f₁ g₁ l ↔ is_O_with c₂ f₂ g₂ l :=
id     └───────┘ └┘ └┘ └┘   └───────┘ └┘ └┘ └┘ 
src    └───────┘             └───────┘
typ    └───────┘ └┘ └┘ └┘   └───────┘ └┘ └┘ └┘ 
doc    └───────┘              └───────┘
116  begin
st   └─────
117    subst c₂,
id           └┘
src    └────┘
typ    └────┘└┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────┘└─
118    apply filter.congr_sets,
id           └───────────────┘
src    └────┘└───────────────┘
typ    └────┘└───────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ────────────────────────┘└─
119    filter_upwards [hf, hg],
src    └──────────────┘  └┘  
typ    └──────────────┘  └┘  
doc    └──────────────┘  └┘  
txt    └──────────────┘  └┘  
par    └──────────────┘  └┘  
pid                  └┘  └┘  
st   ────────────────────────┘└─
120    assume x e₁ e₂,
src    └────────────┘
typ    └────────────┘
doc    └────────────┘
txt    └────────────┘
par    └────────────┘
pid    └────────────┘
st   ───────────────┘└─
121    dsimp at e₁ e₂ ⊢,
src    └──────────────┘
typ    └──────────────┘
doc    └──────────────┘
txt    └──────────────┘
par    └──────────────┘
pid         └────────┘
st   ─────────────────┘└─
122    rw [e₁, e₂]
id         └┘  └┘
src    └──┘  └┘  └┘
typ    └──┘└┘└┘└┘└┘
doc    └──┘  └┘  └┘
txt    └──┘  └┘  └┘
par    └──┘  └┘  └┘
pid      └┘  └┘  
st   ───────┘└──┘
123  end
st   └─┘
124  
125  theorem is_O_with.congr' {c₁ c₂} {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α}
id                                                                     └────┘ 
src                                                                        └────┘
typ                                                                    └────┘ 
126    (hc : c₁ = c₂) (hf : ∀ᶠ x in l, f₁ x = f₂ x) (hg : ∀ᶠ x in l, g₁ x = g₂ x) :
id           └┘  └┘        └┘  └┘  └┘   └┘         └┘  └┘  └┘   └┘ 
src                        └┘   └┘                     └┘   └┘        
typ          └┘  └┘        └┘  └┘  └┘   └┘         └┘  └┘  └┘   └┘ 
doc                         └┘   └┘                      └┘   └┘  
127    is_O_with c₁ f₁ g₁ l → is_O_with c₂ f₂ g₂ l :=
id     └───────┘ └┘ └┘ └┘    └───────┘ └┘ └┘ └┘ 
src    └───────┘              └───────┘
typ    └───────┘ └┘ └┘ └┘    └───────┘ └┘ └┘ └┘ 
doc    └───────┘              └───────┘
128  (is_O_with_congr hc hf hg).mp
id    └─────────────┘ └┘ └┘ └┘ └┘
src   └─────────────┘          └┘
typ   └─────────────┘ └┘ └┘ └┘ └┘
129  
130  theorem is_O_with.congr {c₁ c₂} {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α}
id                                                                    └────┘ 
src                                                                       └────┘
typ                                                                   └────┘ 
131    (hc : c₁ = c₂) (hf : ∀ x, f₁ x = f₂ x) (hg : ∀ x, g₁ x = g₂ x) :
id           └┘  └┘            └┘   └┘             └┘   └┘ 
src                                                         
typ          └┘  └┘            └┘   └┘             └┘   └┘ 
132    is_O_with c₁ f₁ g₁ l → is_O_with c₂ f₂ g₂ l :=
id     └───────┘ └┘ └┘ └┘    └───────┘ └┘ └┘ └┘ 
src    └───────┘              └───────┘
typ    └───────┘ └┘ └┘ └┘    └───────┘ └┘ └┘ └┘ 
doc    └───────┘              └───────┘
133  λ h, h.congr' hc (univ_mem_sets' hf) (univ_mem_sets' hg)
id       └─────┘ └┘  └────────────┘ └┘   └────────────┘ └┘
src        └─────┘     └────────────┘      └────────────┘
typ      └─────┘ └┘  └────────────┘ └┘   └────────────┘ └┘
134  
135  theorem is_O_with.congr_left {f₁ f₂ : α → E} {l : filter α} (hf : ∀ x, f₁ x = f₂ x) :
id                                                   └────┘             └┘   └┘ 
src                                                    └────┘                    
typ                                                  └────┘             └┘   └┘ 
136    is_O_with c f₁ g l → is_O_with c f₂ g l :=
id     └───────┘  └┘     └───────┘  └┘  
src    └───────┘            └───────┘
typ    └───────┘  └┘     └───────┘  └┘  
doc    └───────┘            └───────┘
137  is_O_with.congr rfl hf (λ _, rfl)
id   └─────────────┘ └─┘ └┘      └─┘
src  └─────────────┘ └─┘          └─┘
typ  └─────────────┘ └─┘ └┘      └─┘
138  
139  theorem is_O_with.congr_right {g₁ g₂ : α → F} {l : filter α} (hg : ∀ x, g₁ x = g₂ x) :
id                                                    └────┘             └┘   └┘ 
src                                                     └────┘                    
typ                                                   └────┘             └┘   └┘ 
140    is_O_with c f g₁ l → is_O_with c f g₂ l :=
id     └───────┘   └┘    └───────┘   └┘ 
src    └───────┘            └───────┘
typ    └───────┘   └┘    └───────┘   └┘ 
doc    └───────┘            └───────┘
141  is_O_with.congr rfl (λ _, rfl) hg
id   └─────────────┘ └─┘      └─┘  └┘
src  └─────────────┘ └─┘       └─┘
typ  └─────────────┘ └─┘      └─┘  └┘
142  
143  theorem is_O_with.congr_const {c₁ c₂} {l : filter α} (hc : c₁ = c₂) :
id                                              └────┘         └┘  └┘
src                                             └────┘             
typ                                             └────┘         └┘  └┘
144    is_O_with c₁ f g l → is_O_with c₂ f g l :=
id     └───────┘ └┘      └───────┘ └┘   
src    └───────┘            └───────┘
typ    └───────┘ └┘      └───────┘ └┘   
doc    └───────┘            └───────┘
145  is_O_with.congr hc (λ _, rfl) (λ _, rfl)
id   └─────────────┘ └┘      └─┘       └─┘
src  └─────────────┘          └─┘        └─┘
typ  └─────────────┘ └┘      └─┘       └─┘
146  
147  theorem is_O_congr {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α}
id                                                       └────┘ 
src                                                          └────┘
typ                                                      └────┘ 
148      (hf : ∀ᶠ x in l, f₁ x = f₂ x) (hg : ∀ᶠ x in l, g₁ x = g₂ x) :
id             └┘  └┘  └┘   └┘         └┘  └┘  └┘   └┘ 
src            └┘   └┘                     └┘   └┘        
typ            └┘  └┘  └┘   └┘         └┘  └┘  └┘   └┘ 
doc            └┘   └┘                      └┘   └┘  
149    is_O f₁ g₁ l ↔ is_O f₂ g₂ l :=
id     └──┘ └┘ └┘   └──┘ └┘ └┘ 
src    └──┘          └──┘
typ    └──┘ └┘ └┘   └──┘ └┘ └┘ 
doc    └──┘           └──┘
150  exists_congr $ λ c, is_O_with_congr rfl hf hg
id   └──────────┘       └─────────────┘ └─┘ └┘ └┘
src  └──────────┘        └─────────────┘ └─┘
typ  └──────────┘       └─────────────┘ └─┘ └┘ └┘
151  
152  theorem is_O.congr' {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α}
id                                                        └────┘ 
src                                                           └────┘
typ                                                       └────┘ 
153    (hf : ∀ᶠ x in l, f₁ x = f₂ x) (hg : ∀ᶠ x in l, g₁ x = g₂ x) :
id           └┘  └┘  └┘   └┘         └┘  └┘  └┘   └┘ 
src          └┘   └┘                     └┘   └┘        
typ          └┘  └┘  └┘   └┘         └┘  └┘  └┘   └┘ 
doc          └┘   └┘                      └┘   └┘  
154    is_O f₁ g₁ l → is_O f₂ g₂ l :=
id     └──┘ └┘ └┘    └──┘ └┘ └┘ 
src    └──┘           └──┘
typ    └──┘ └┘ └┘    └──┘ └┘ └┘ 
doc    └──┘           └──┘
155  (is_O_congr hf hg).mp
id    └────────┘ └┘ └┘ └┘
src   └────────┘       └┘
typ   └────────┘ └┘ └┘ └┘
156  
157  theorem is_O.congr {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α}
id                                                       └────┘ 
src                                                          └────┘
typ                                                      └────┘ 
158      (hf : ∀ x, f₁ x = f₂ x) (hg : ∀ x, g₁ x = g₂ x) :
id                 └┘   └┘             └┘   └┘ 
src                                             
typ                └┘   └┘             └┘   └┘ 
159    is_O f₁ g₁ l → is_O f₂ g₂ l :=
id     └──┘ └┘ └┘    └──┘ └┘ └┘ 
src    └──┘           └──┘
typ    └──┘ └┘ └┘    └──┘ └┘ └┘ 
doc    └──┘           └──┘
160  λ h, h.congr' (univ_mem_sets' hf) (univ_mem_sets' hg)
id       └─────┘  └────────────┘ └┘   └────────────┘ └┘
src        └─────┘  └────────────┘      └────────────┘
typ      └─────┘  └────────────┘ └┘   └────────────┘ └┘
161  
162  theorem is_O.congr_left {f₁ f₂ : α → E} {l : filter α} (hf : ∀ x, f₁ x = f₂ x) :
id                                              └────┘             └┘   └┘ 
src                                               └────┘                    
typ                                             └────┘             └┘   └┘ 
163    is_O f₁ g l → is_O f₂ g l :=
id     └──┘ └┘     └──┘ └┘  
src    └──┘          └──┘
typ    └──┘ └┘     └──┘ └┘  
doc    └──┘          └──┘
164  is_O.congr hf (λ _, rfl)
id   └────────┘ └┘      └─┘
src  └────────┘          └─┘
typ  └────────┘ └┘      └─┘
165  
166  theorem is_O.congr_right {g₁ g₂ : α → E} {l : filter α} (hg : ∀ x, g₁ x = g₂ x) :
id                                               └────┘             └┘   └┘ 
src                                                └────┘                    
typ                                              └────┘             └┘   └┘ 
167    is_O f g₁ l → is_O f g₂ l :=
id     └──┘  └┘    └──┘  └┘ 
src    └──┘          └──┘
typ    └──┘  └┘    └──┘  └┘ 
doc    └──┘          └──┘
168  is_O.congr (λ _, rfl) hg
id   └────────┘      └─┘  └┘
src  └────────┘       └─┘
typ  └────────┘      └─┘  └┘
169  
170  theorem is_o_congr {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α}
id                                                       └────┘ 
src                                                          └────┘
typ                                                      └────┘ 
171      (hf : ∀ᶠ x in l, f₁ x = f₂ x) (hg : ∀ᶠ x in l, g₁ x = g₂ x) :
id             └┘  └┘  └┘   └┘         └┘  └┘  └┘   └┘ 
src            └┘   └┘                     └┘   └┘        
typ            └┘  └┘  └┘   └┘         └┘  └┘  └┘   └┘ 
doc            └┘   └┘                      └┘   └┘  
172    is_o f₁ g₁ l ↔ is_o f₂ g₂ l :=
id     └──┘ └┘ └┘   └──┘ └┘ └┘ 
src    └──┘          └──┘
typ    └──┘ └┘ └┘   └──┘ └┘ └┘ 
doc    └──┘           └──┘
173  ball_congr (λ c hc, is_O_with_congr (eq.refl c) hf hg)
id   └────────┘     └┘  └─────────────┘  └─────┘   └┘ └┘
src  └────────┘          └─────────────┘  └─────┘
typ  └────────┘     └┘  └─────────────┘  └─────┘   └┘ └┘
174  
175  theorem is_o.congr' {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α}
id                                                        └────┘ 
src                                                           └────┘
typ                                                       └────┘ 
176    (hf : ∀ᶠ x in l, f₁ x = f₂ x) (hg : ∀ᶠ x in l, g₁ x = g₂ x) :
id           └┘  └┘  └┘   └┘         └┘  └┘  └┘   └┘ 
src          └┘   └┘                     └┘   └┘        
typ          └┘  └┘  └┘   └┘         └┘  └┘  └┘   └┘ 
doc          └┘   └┘                      └┘   └┘  
177    is_o f₁ g₁ l → is_o f₂ g₂ l :=
id     └──┘ └┘ └┘    └──┘ └┘ └┘ 
src    └──┘           └──┘
typ    └──┘ └┘ └┘    └──┘ └┘ └┘ 
doc    └──┘           └──┘
178  (is_o_congr hf hg).mp
id    └────────┘ └┘ └┘ └┘
src   └────────┘       └┘
typ   └────────┘ └┘ └┘ └┘
179  
180  theorem is_o.congr {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α}
id                                                       └────┘ 
src                                                          └────┘
typ                                                      └────┘ 
181      (hf : ∀ x, f₁ x = f₂ x) (hg : ∀ x, g₁ x = g₂ x) :
id                 └┘   └┘             └┘   └┘ 
src                                             
typ                └┘   └┘             └┘   └┘ 
182    is_o f₁ g₁ l → is_o f₂ g₂ l :=
id     └──┘ └┘ └┘    └──┘ └┘ └┘ 
src    └──┘           └──┘
typ    └──┘ └┘ └┘    └──┘ └┘ └┘ 
doc    └──┘           └──┘
183  λ h, h.congr' (univ_mem_sets' hf) (univ_mem_sets' hg)
id       └─────┘  └────────────┘ └┘   └────────────┘ └┘
src        └─────┘  └────────────┘      └────────────┘
typ      └─────┘  └────────────┘ └┘   └────────────┘ └┘
184  
185  theorem is_o.congr_left {f₁ f₂ : α → E} {l : filter α} (hf : ∀ x, f₁ x = f₂ x) :
id                                              └────┘             └┘   └┘ 
src                                               └────┘                    
typ                                             └────┘             └┘   └┘ 
186    is_o f₁ g l → is_o f₂ g l :=
id     └──┘ └┘     └──┘ └┘  
src    └──┘          └──┘
typ    └──┘ └┘     └──┘ └┘  
doc    └──┘          └──┘
187  is_o.congr hf (λ _, rfl)
id   └────────┘ └┘      └─┘
src  └────────┘          └─┘
typ  └────────┘ └┘      └─┘
188  
189  theorem is_o.congr_right {g₁ g₂ : α → E} {l : filter α} (hg : ∀ x, g₁ x = g₂ x) :
id                                               └────┘             └┘   └┘ 
src                                                └────┘                    
typ                                              └────┘             └┘   └┘ 
190    is_o f g₁ l → is_o f g₂ l :=
id     └──┘  └┘    └──┘  └┘ 
src    └──┘          └──┘
typ    └──┘  └┘    └──┘  └┘ 
doc    └──┘          └──┘
191  is_o.congr (λ _, rfl) hg
id   └────────┘      └─┘  └┘
src  └────────┘       └─┘
typ  └────────┘      └─┘  └┘
192  
193  /-! ### Filter operations and transitivity -/
194  
195  theorem is_O_with.comp_tendsto (hcfg : is_O_with c f g l)
id                                          └───────┘    
src                                         └───────┘
typ                                         └───────┘    
doc                                         └───────┘
196    {k : β → α} {l' : filter β} (hk : tendsto k l' l):
id                     └────┘         └─────┘  └┘ 
src                      └────┘          └─────┘
typ                    └────┘         └─────┘  └┘ 
doc                                      └─────┘
197    is_O_with c (f ∘ k) (g ∘ k) l' :=
id     └───────┘            └┘
src    └───────┘             
typ    └───────┘            └┘
doc    └───────┘
198  hk hcfg
id   └┘ └──┘
typ  └┘ └──┘
199  
200  theorem is_O.comp_tendsto (hfg : is_O f g l) {k : β → α} {l' : filter β} (hk : tendsto k l' l) :
id                                    └──┘                     └────┘         └─────┘  └┘ 
src                                   └──┘                          └────┘          └─────┘
typ                                   └──┘                     └────┘         └─────┘  └┘ 
doc                                   └──┘                                          └─────┘
201    is_O (f ∘ k) (g ∘ k) l' :=
id     └──┘           └┘
src    └──┘           
typ    └──┘           └┘
doc    └──┘
202  hfg.imp (λ c h, h.comp_tendsto hk)
id   └─┘└──┘       └───────────┘ └┘
src     └──┘          └───────────┘
typ  └─┘└──┘       └───────────┘ └┘
203  
204  theorem is_o.comp_tendsto (hfg : is_o f g l) {k : β → α} {l' : filter β} (hk : tendsto k l' l) :
id                                    └──┘                     └────┘         └─────┘  └┘ 
src                                   └──┘                          └────┘          └─────┘
typ                                   └──┘                     └────┘         └─────┘  └┘ 
doc                                   └──┘                                          └─────┘
205    is_o (f ∘ k) (g ∘ k) l' :=
id     └──┘           └┘
src    └──┘           
typ    └──┘           └┘
doc    └──┘
206  λ c cpos, (hfg cpos).comp_tendsto hk
id      └──┘   └─┘ └──┘ └──────────┘  └┘
src                      └──────────┘
typ     └──┘   └─┘ └──┘ └──────────┘  └┘
207  
208  theorem is_O_with.mono (h : is_O_with c f g l') (hl : l ≤ l') : is_O_with c f g l :=
id                               └───────┘    └┘          └┘    └───────┘    
src                              └───────┘                          └───────┘
typ                              └───────┘    └┘          └┘    └───────┘    
doc                              └───────┘                           └───────┘
209  hl h
id   └┘ 
typ  └┘ 
210  
211  theorem is_O.mono (h : is_O f g l') (hl : l ≤ l') : is_O f g l :=
id                          └──┘   └┘          └┘    └──┘   
src                         └──┘                        └──┘
typ                         └──┘   └┘          └┘    └──┘   
doc                         └──┘                         └──┘
212  h.imp (λ c h, h.mono hl)
id   └──┘       └───┘ └┘
src   └──┘          └───┘
typ  └──┘       └───┘ └┘
213  
214  theorem is_o.mono (h : is_o f g l') (hl : l ≤ l') : is_o f g l :=
id                          └──┘   └┘          └┘    └──┘   
src                         └──┘                        └──┘
typ                         └──┘   └┘          └┘    └──┘   
doc                         └──┘                         └──┘
215  λ c cpos, (h cpos).mono hl
id      └──┘    └──┘ └──┘  └┘
src                    └──┘
typ     └──┘    └──┘ └──┘  └┘
216  
217  theorem is_O_with.trans (hfg : is_O_with c f g l) (hgk : is_O_with c' g k l) (hc : 0 ≤ c) :
id                                  └───────┘             └───────┘ └┘              
src                                 └───────┘                 └───────┘                   
typ                                 └───────┘             └───────┘ └┘              
doc                                 └───────┘                 └───────┘
218    is_O_with (c * c') f k l :=
id     └───────┘    └┘    
src    └───────┘    
typ    └───────┘    └┘    
doc    └───────┘
219  begin
st   └─────
220    filter_upwards [hfg, hgk],
src    └──────────────┘   └┘   
typ    └──────────────┘   └┘   
doc    └──────────────┘   └┘   
txt    └──────────────┘   └┘   
par    └──────────────┘   └┘   
pid                  └┘   └┘   
st   ──────────────────────────┘└─
221    assume x hx hx',
src    └─────────────┘
typ    └─────────────┘
doc    └─────────────┘
txt    └─────────────┘
par    └─────────────┘
pid    └─────────────┘
st   ────────────────┘└─
222    calc ∥f x∥ ≤ c * ∥g x∥ : hx
id     └──┘               └┘
src    └──┘    
typ    └──┘               └┘
doc    └──┘
st   ──────────────────────────────
223    ... ≤ c * (c' * ∥k x∥) : mul_le_mul_of_nonneg_left hx' hc
id                             └───────────────────────┘ └─┘ └┘
src                            └───────────────────────┘
typ                            └───────────────────────┘ └─┘ └┘
st   ────────────────────────────────────────────────────────────
224    ... = c * c' * ∥k x∥ : (mul_assoc _ _ _).symm
id               └┘           └───────┘       └──┘
src                            └───────┘       └──┘
typ              └┘           └───────┘       └──┘
st   ─────────────────────────────────────────────┘└─
225  end
st   ──┘
226  
227  theorem is_O.trans (hfg : is_O f g' l) (hgk : is_O g' k l) : is_O f k l :=
id                             └──┘  └┘          └──┘ └┘      └──┘   
src                            └──┘                └──┘           └──┘
typ                            └──┘  └┘          └──┘ └┘      └──┘   
doc                            └──┘                └──┘           └──┘
228  let ⟨c, cnonneg, hc⟩ := hfg.exists_nonneg, ⟨c', hc'⟩ := hgk in (hc.trans hc' cnonneg).is_O
id   └─┘     └─────┘  └┘     └─┘└────────────┘       └─┘     └─┘       └────┘             └──┘
src                             └────────────┘                         └────┘             └──┘
typ  └─┘     └─────┘  └┘     └─┘└────────────┘       └─┘     └─┘       └────┘             └──┘
229  
230  theorem is_o.trans_is_O_with (hfg : is_o f g l) (hgk : is_O_with c g k l) (hc : 0 < c) :
id                                       └──┘            └───────┘               
src                                      └──┘               └───────┘                  
typ                                      └──┘            └───────┘               
doc                                      └──┘               └───────┘
231    is_o f k l :=
id     └──┘   
src    └──┘
typ    └──┘   
doc    └──┘
232  begin
st   └─────
233    intros c' c'pos,
src    └─────────────┘
typ    └─────────────┘
doc    └─────────────┘
txt    └─────────────┘
par    └─────────────┘
pid          └───────┘
st   ────────────────┘└─
234    have : 0 < c' / c, from div_pos c'pos hc,
id               └┘         └─────┘ └───┘ └┘
src    └───────┘     └───┘└─────┘     
typ    └───────┘└┘  └───┘└─────┘└───┘└┘
doc    └───────┘       └───┘            
txt    └───────┘       └───┘            
par    └───────┘       └───┘            
pid    └───┘└──┘       └───┘            
st   ──────────────────┘└─────────────────────┘└─
235    exact ((hfg this).trans hgk (le_of_lt this)).congr_const (div_mul_cancel _ (ne_of_gt hc))
id             └─┘             └─┘  └──────┘ └──┘                └────────────┘    └──────┘ └┘
src    └────┘         └──────┘    └──────┘    └─────────────┘ └────────────┘└─┘ └──────┘  └─┘
typ    └────┘  └─┘    └──────┘└─┘ └──────┘└──┘└─────────────┘ └────────────┘└─┘ └──────┘└┘└─┘
doc    └────┘         └──────┘                └─────────────┘               └─┘           └─┘
txt    └────┘         └──────┘                └─────────────┘               └─┘           └─┘
par    └────┘         └──────┘                └─────────────┘               └─┘           └─┘
pid                  └──────┘                └─────────────┘               └─┘           └┘
st   ───────────────────────────────────────────────────────────────────────────────────────────┘
236  end
st   └─┘
237  
238  theorem is_o.trans_is_O (hfg : is_o f g l) (hgk : is_O g k' l) : is_o f k' l :=
id                                  └──┘            └──┘  └┘     └──┘  └┘ 
src                                 └──┘               └──┘           └──┘
typ                                 └──┘            └──┘  └┘     └──┘  └┘ 
doc                                 └──┘               └──┘           └──┘
239  let ⟨c, cpos, hc⟩ := hgk.exists_pos in hfg.trans_is_O_with hc cpos
id   └─┘     └──┘  └┘     └─┘└─────────┘    └─┘└──────────────┘
src                          └─────────┘       └──────────────┘
typ  └─┘     └──┘  └┘     └─┘└─────────┘    └─┘└──────────────┘
240  
241  theorem is_O_with.trans_is_o (hfg : is_O_with c f g l) (hgk : is_o g k l) (hc : 0 < c) :
id                                       └───────┘             └──┘              
src                                      └───────┘                 └──┘                
typ                                      └───────┘             └──┘              
doc                                      └───────┘                 └──┘
242    is_o f k l :=
id     └──┘   
src    └──┘
typ    └──┘   
doc    └──┘
243  begin
st   └─────
244    intros c' c'pos,
src    └─────────────┘
typ    └─────────────┘
doc    └─────────────┘
txt    └─────────────┘
par    └─────────────┘
pid          └───────┘
st   ────────────────┘└─
245    have : 0 < c' / c, from div_pos c'pos hc,
id               └┘         └─────┘ └───┘ └┘
src    └───────┘     └───┘└─────┘     
typ    └───────┘└┘  └───┘└─────┘└───┘└┘
doc    └───────┘       └───┘            
txt    └───────┘       └───┘            
par    └───────┘       └───┘            
pid    └───┘└──┘       └───┘            
st   ──────────────────┘└─────────────────────┘└─
246    exact (hfg.trans (hgk this) (le_of_lt hc)).congr_const (mul_div_cancel' _ (ne_of_gt hc))
id            └───────┘  └─┘ └──┘   └──────┘                   └─────────────┘    └──────┘ └┘
src    └────┘ └───────┘        └┘ └──────┘  └─────────────┘ └─────────────┘└─┘ └──────┘  └─┘
typ    └────┘ └───────┘ └─┘└──┘└┘ └──────┘  └─────────────┘ └─────────────┘└─┘ └──────┘└┘└─┘
doc    └────┘                  └┘           └─────────────┘                └─┘           └─┘
txt    └────┘                  └┘           └─────────────┘                └─┘           └─┘
par    └────┘                  └┘           └─────────────┘                └─┘           └─┘
pid                           └┘           └─────────────┘                └─┘           └┘
st   ──────────────────────────────────────────────────────────────────────────────────────────┘
247  end
st   └─┘
248  
249  theorem is_O.trans_is_o (hfg : is_O f g' l) (hgk : is_o g' k l) : is_o f k l :=
id                                  └──┘  └┘          └──┘ └┘      └──┘   
src                                 └──┘                └──┘           └──┘
typ                                 └──┘  └┘          └──┘ └┘      └──┘   
doc                                 └──┘                └──┘           └──┘
250  let ⟨c, cpos, hc⟩ := hfg.exists_pos in hc.trans_is_o hgk cpos
id   └─┘     └──┘  └┘     └─┘└─────────┘      └─────────┘ └─┘
src                          └─────────┘      └─────────┘
typ  └─┘     └──┘  └┘     └─┘└─────────┘      └─────────┘ └─┘
251  
252  theorem is_o.trans (hfg : is_o f g l) (hgk : is_o g k' l) : is_o f k' l :=
id                             └──┘            └──┘  └┘     └──┘  └┘ 
src                            └──┘               └──┘           └──┘
typ                            └──┘            └──┘  └┘     └──┘  └┘ 
doc                            └──┘               └──┘           └──┘
253  hfg.trans_is_O hgk.is_O
id   └─┘└─────────┘ └─┘└───┘
src     └─────────┘    └───┘
typ  └─┘└─────────┘ └─┘└───┘
254  
255  theorem is_o.trans' (hfg : is_o f g' l) (hgk : is_o g' k l) : is_o f k l :=
id                              └──┘  └┘          └──┘ └┘      └──┘   
src                             └──┘                └──┘           └──┘
typ                             └──┘  └┘          └──┘ └┘      └──┘   
doc                             └──┘                └──┘           └──┘
256  hfg.is_O.trans_is_o hgk
id   └─┘└───┘└─────────┘ └─┘
src     └───┘└─────────┘
typ  └─┘└───┘└─────────┘ └─┘
257  
258  section
259  
260  variable (l)
261  
262  theorem is_O_with_of_le' (hfg : ∀ x, ∥f x∥ ≤ c * ∥g x∥) : is_O_with c f g l :=
id                                                 └───────┘    
src                                                      └───────┘
typ                                                └───────┘    
doc                                                            └───────┘
263  univ_mem_sets' hfg
id   └────────────┘ └─┘
src  └────────────┘
typ  └────────────┘ └─┘
264  
265  theorem is_O_with_of_le (hfg : ∀ x, ∥f x∥ ≤ ∥g x∥) : is_O_with 1 f g l :=
id                                              └───────┘     
src                                                  └───────┘
typ                                             └───────┘     
doc                                                       └───────┘
266  is_O_with_of_le' l $ λ x, by { rw one_mul, exact hfg x }
id   └──────────────┘                └─────┘        └─┘ 
src  └──────────────┘               └─┘└─────┘  └────┘    
typ  └──────────────┘             └─┘└─────┘  └────┘└─┘
doc                                 └─┘         └────┘    
txt                                 └─┘         └────┘    
par                                 └─┘         └────┘    
pid                                                     
st                               └───────────┘└────────────┘└┘
267  
268  theorem is_O_of_le' (hfg : ∀ x, ∥f x∥ ≤ c * ∥g x∥) : is_O f g l :=
id                                            └──┘   
src                                                 └──┘
typ                                           └──┘   
doc                                                       └──┘
269  (is_O_with_of_le' l hfg).is_O
id    └──────────────┘  └─┘ └──┘
src   └──────────────┘       └──┘
typ   └──────────────┘  └─┘ └──┘
270  
271  theorem is_O_of_le (hfg : ∀ x, ∥f x∥ ≤ ∥g x∥) : is_O f g l :=
id                                         └──┘   
src                                             └──┘
typ                                        └──┘   
doc                                                  └──┘
272  (is_O_with_of_le l hfg).is_O
id    └─────────────┘  └─┘ └──┘
src   └─────────────┘       └──┘
typ   └─────────────┘  └─┘ └──┘
273  
274  end
275  
276  theorem is_O_with_refl (f : α → E) (l : filter α) : is_O_with 1 f f l :=
id                                         └────┘     └───────┘     
src                                          └────┘      └───────┘
typ                                        └────┘     └───────┘     
doc                                                      └───────┘
277  is_O_with_of_le l $ λ _, le_refl _
id   └─────────────┘        └─────┘
src  └─────────────┘          └─────┘
typ  └─────────────┘        └─────┘
278  
279  theorem is_O_refl (f : α → E) (l : filter α) : is_O f f l := (is_O_with_refl f l).is_O
id                                    └────┘     └──┘        └────────────┘   └──┘
src                                     └────┘      └──┘           └────────────┘     └──┘
typ                                   └────┘     └──┘        └────────────┘   └──┘
doc                                                 └──┘
280  
281  theorem is_O_with.trans_le (hfg : is_O_with c f g l) (hgk : ∀ x, ∥g x∥ ≤ ∥k x∥) (hc : 0 ≤ c) :
id                                     └───────┘                                
src                                    └───────┘                                        
typ                                    └───────┘                                
doc                                    └───────┘
282    is_O_with c f k l :=
id     └───────┘    
src    └───────┘
typ    └───────┘    
doc    └───────┘
283  (hfg.trans (is_O_with_of_le l hgk) hc).congr_const $ mul_one c
id    └─┘└────┘  └─────────────┘  └─┘  └┘ └─────────┘    └─────┘ 
src      └────┘  └─────────────┘           └─────────┘    └─────┘
typ   └─┘└────┘  └─────────────┘  └─┘  └┘ └─────────┘    └─────┘ 
284  
285  theorem is_O.trans_le (hfg : is_O f g' l) (hgk : ∀ x, ∥g' x∥ ≤ ∥k x∥) :
id                                └──┘  └┘              └┘    
src                               └──┘                              
typ                               └──┘  └┘              └┘    
doc                               └──┘
286    is_O f k l :=
id     └──┘   
src    └──┘
typ    └──┘   
doc    └──┘
287  hfg.trans (is_O_of_le l hgk)
id   └─┘└────┘  └────────┘  └─┘
src     └────┘  └────────┘
typ  └─┘└────┘  └────────┘  └─┘
288  
289  section bot
290  
291  variables (c f g)
292  
293  theorem is_O_with_bot : is_O_with c f g ⊥ := trivial
id                           └───────┘        └─────┘
src                          └───────┘           └─────┘
typ                          └───────┘        └─────┘
doc                          └───────┘
294  
295  theorem is_O_bot : is_O f g ⊥ := (is_O_with_bot c f g).is_O
id                      └──┘        └───────────┘    └──┘
src                     └──┘          └───────────┘       └──┘
typ                     └──┘        └───────────┘    └──┘
doc                     └──┘
296  
297  theorem is_o_bot : is_o f g ⊥ := λ c _, is_O_with_bot c f g
id                      └──┘            └───────────┘   
src                     └──┘                └───────────┘
typ                     └──┘            └───────────┘   
doc                     └──┘
298  
299  end bot
300  
301  theorem is_O_with.join (h : is_O_with c f g l) (h' : is_O_with c f g l') :
id                               └───────┘            └───────┘    └┘
src                              └───────┘                └───────┘
typ                              └───────┘            └───────┘    └┘
doc                              └───────┘                └───────┘
302    is_O_with c f g (l ⊔ l') :=
id     └───────┘       └┘
src    └───────┘          
typ    └───────┘       └┘
doc    └───────┘
303  mem_sup_sets.2 ⟨h, h'⟩
id   └──────────┘     └┘
src  └──────────┘
typ  └──────────┘     └┘
304  
305  theorem is_O_with.join' (h : is_O_with c f g' l) (h' : is_O_with c' f g' l') :
id                                └───────┘   └┘         └───────┘ └┘  └┘ └┘
src                               └───────┘                 └───────┘
typ                               └───────┘   └┘         └───────┘ └┘  └┘ └┘
doc                               └───────┘                 └───────┘
306    is_O_with (max c c') f g' (l ⊔ l') :=
id     └───────┘  └─┘  └┘   └┘    └┘
src    └───────┘  └─┘               
typ    └───────┘  └─┘  └┘   └┘    └┘
doc    └───────┘
307  mem_sup_sets.2 ⟨(h.weaken $ le_max_left c c'), (h'.weaken $ le_max_right c c')⟩
id   └──────────┘    └─────┘   └─────────┘  └┘    └┘└─────┘   └──────────┘  └┘
src  └──────────┘     └─────┘   └─────────┘           └─────┘   └──────────┘
typ  └──────────┘    └─────┘   └─────────┘  └┘    └┘└─────┘   └──────────┘  └┘
308  
309  theorem is_O.join (h : is_O f g' l) (h' : is_O f g' l') : is_O f g' (l ⊔ l') :=
id                          └──┘  └┘         └──┘  └┘ └┘    └──┘  └┘    └┘
src                         └──┘               └──┘            └──┘         
typ                         └──┘  └┘         └──┘  └┘ └┘    └──┘  └┘    └┘
doc                         └──┘               └──┘            └──┘
310  let ⟨c, hc⟩ := h, ⟨c', hc'⟩ := h' in (hc.join' hc').is_O
id   └─┘     └┘            └─┘     └┘       └────┘     └──┘
src                                          └────┘     └──┘
typ  └─┘     └┘            └─┘     └┘       └────┘     └──┘
311  
312  theorem is_o.join (h : is_o f g l) (h' : is_o f g l') :
id                          └──┘           └──┘   └┘
src                         └──┘              └──┘
typ                         └──┘           └──┘   └┘
doc                         └──┘              └──┘
313    is_o f g (l ⊔ l') :=
id     └──┘      └┘
src    └──┘        
typ    └──┘      └┘
doc    └──┘
314  λ c cpos, (h cpos).join (h' cpos)
id      └──┘    └──┘ └──┘   └┘ └──┘
src                    └──┘
typ     └──┘    └──┘ └──┘   └┘ └──┘
315  
316  /-! ### Simplification : norm -/
317  
318  @[simp] theorem is_O_with_norm_right : is_O_with c f (λ x, ∥g' x∥) l ↔ is_O_with c f g' l :=
id                                          └───────┘        └┘     └───────┘   └┘ 
src                                         └───────┘                    └───────┘
typ                                         └───────┘        └┘     └───────┘   └┘ 
doc    └──┘                                 └───────┘                       └───────┘
319  by simp only [is_O_with, norm_norm]
id                 └───────┘  └───────┘
src     └─────────┘└───────┘└┘└───────┘└─
typ     └─────────┘└───────┘└┘└───────┘└─
doc     └─────────┘└───────┘└┘         └─
txt     └─────────┘         └┘         └─
par     └─────────┘         └┘         └─
pid         └──┘└┘         └┘         
st     └─────────────────────────────────
320  
src  
typ  
doc  
txt  
par  
pid  
st   
321  alias is_O_with_norm_right ↔ asymptotics.is_O_with.of_norm_right asymptotics.is_O_with.norm_right
322  
323  @[simp] theorem is_O_norm_right : is_O f (λ x, ∥g' x∥) l ↔ is_O f g' l :=
id                                     └──┘       └┘     └──┘  └┘ 
src                                    └──┘                  └──┘
typ                                    └──┘       └┘     └──┘  └┘ 
doc    └──┘                            └──┘                     └──┘
324  exists_congr $ λ _,  is_O_with_norm_right
id   └──────────┘        └──────────────────┘
src  └──────────┘         └──────────────────┘
typ  └──────────┘        └──────────────────┘
325  
326  alias is_O_norm_right ↔ asymptotics.is_O.of_norm_right asymptotics.is_O.norm_right
327  
328  @[simp] theorem is_o_norm_right : is_o f (λ x, ∥g' x∥) l ↔ is_o f g' l :=
id                                     └──┘       └┘     └──┘  └┘ 
src                                    └──┘                  └──┘
typ                                    └──┘       └┘     └──┘  └┘ 
doc    └──┘                            └──┘                     └──┘
329  forall_congr $ λ _, forall_congr $ λ _, is_O_with_norm_right
id   └──────────┘       └──────────┘       └──────────────────┘
src  └──────────┘        └──────────┘        └──────────────────┘
typ  └──────────┘       └──────────┘       └──────────────────┘
330  
331  alias is_o_norm_right ↔ asymptotics.is_o.of_norm_right asymptotics.is_o.norm_right
332  
333  @[simp] theorem is_O_with_norm_left : is_O_with c (λ x, ∥f' x∥) g l ↔ is_O_with c f' g l :=
id                                         └───────┘       └┘      └───────┘  └┘  
src                                        └───────┘                    └───────┘
typ                                        └───────┘       └┘      └───────┘  └┘  
doc    └──┘                                └───────┘                       └───────┘
334  by simp only [is_O_with, norm_norm]
id                 └───────┘  └───────┘
src     └─────────┘└───────┘└┘└───────┘└─
typ     └─────────┘└───────┘└┘└───────┘└─
doc     └─────────┘└───────┘└┘         └─
txt     └─────────┘         └┘         └─
par     └─────────┘         └┘         └─
pid         └──┘└┘         └┘         
st     └─────────────────────────────────
335  
src  
typ  
doc  
txt  
par  
pid  
st   
336  alias is_O_with_norm_left ↔ asymptotics.is_O_with.of_norm_left asymptotics.is_O_with.norm_left
337  
338  @[simp] theorem is_O_norm_left : is_O (λ x, ∥f' x∥) g l ↔ is_O f' g l :=
id                                    └──┘      └┘      └──┘ └┘  
src                                   └──┘                  └──┘
typ                                   └──┘      └┘      └──┘ └┘  
doc    └──┘                           └──┘                     └──┘
339  exists_congr $ λ _, is_O_with_norm_left
id   └──────────┘       └─────────────────┘
src  └──────────┘        └─────────────────┘
typ  └──────────┘       └─────────────────┘
340  
341  alias is_O_norm_left ↔ asymptotics.is_O.of_norm_left asymptotics.is_O.norm_left
342  
343  @[simp] theorem is_o_norm_left : is_o (λ x, ∥f' x∥) g l ↔ is_o f' g l :=
id                                    └──┘      └┘      └──┘ └┘  
src                                   └──┘                  └──┘
typ                                   └──┘      └┘      └──┘ └┘  
doc    └──┘                           └──┘                     └──┘
344  forall_congr $ λ _, forall_congr $ λ _, is_O_with_norm_left
id   └──────────┘       └──────────┘       └─────────────────┘
src  └──────────┘        └──────────┘        └─────────────────┘
typ  └──────────┘       └──────────┘       └─────────────────┘
345  
346  alias is_o_norm_left ↔ asymptotics.is_o.of_norm_left asymptotics.is_o.norm_left
347  
348  theorem is_O_with_norm_norm :
349    is_O_with c (λ x, ∥f' x∥) (λ x, ∥g' x∥) l ↔ is_O_with c f' g' l :=
id     └───────┘       └┘        └┘     └───────┘  └┘ └┘ 
src    └───────┘                              └───────┘
typ    └───────┘       └┘        └┘     └───────┘  └┘ └┘ 
doc    └───────┘                                   └───────┘
350  is_O_with_norm_left.trans is_O_with_norm_right
id   └─────────────────┘└────┘ └──────────────────┘
src  └─────────────────┘└────┘ └──────────────────┘
typ  └─────────────────┘└────┘ └──────────────────┘
351  
352  alias is_O_with_norm_norm ↔ asymptotics.is_O_with.of_norm_norm asymptotics.is_O_with.norm_norm
353  
354  theorem is_O_norm_norm :
355    is_O (λ x, ∥f' x∥) (λ x, ∥g' x∥) l ↔ is_O f' g' l :=
id     └──┘      └┘        └┘     └──┘ └┘ └┘ 
src    └──┘                            └──┘
typ    └──┘      └┘        └┘     └──┘ └┘ └┘ 
doc    └──┘                                 └──┘
356  is_O_norm_left.trans is_O_norm_right
id   └────────────┘└────┘ └─────────────┘
src  └────────────┘└────┘ └─────────────┘
typ  └────────────┘└────┘ └─────────────┘
357  
358  alias is_O_norm_norm ↔ asymptotics.is_O.of_norm_norm asymptotics.is_O.norm_norm
359  
360  theorem is_o_norm_norm :
361    is_o (λ x, ∥f' x∥) (λ x, ∥g' x∥) l ↔ is_o f' g' l :=
id     └──┘      └┘        └┘     └──┘ └┘ └┘ 
src    └──┘                            └──┘
typ    └──┘      └┘        └┘     └──┘ └┘ └┘ 
doc    └──┘                                 └──┘
362  is_o_norm_left.trans is_o_norm_right
id   └────────────┘└────┘ └─────────────┘
src  └────────────┘└────┘ └─────────────┘
typ  └────────────┘└────┘ └─────────────┘
363  
364  alias is_o_norm_norm ↔ asymptotics.is_o.of_norm_norm asymptotics.is_o.norm_norm
365  
366  /-! ### Simplification: negate -/
367  
368  @[simp] theorem is_O_with_neg_right : is_O_with c f (λ x, -(g' x)) l ↔ is_O_with c f g' l :=
id                                         └───────┘         └┘      └───────┘   └┘ 
src                                        └───────┘                      └───────┘
typ                                        └───────┘         └┘      └───────┘   └┘ 
doc    └──┘                                └───────┘                        └───────┘
369  by simp only [is_O_with, norm_neg]
id                 └───────┘  └──────┘
src     └─────────┘└───────┘└┘└──────┘└─
typ     └─────────┘└───────┘└┘└──────┘└─
doc     └─────────┘└───────┘└┘        └─
txt     └─────────┘         └┘        └─
par     └─────────┘         └┘        └─
pid         └──┘└┘         └┘        
st     └────────────────────────────────
370  
src  
typ  
doc  
txt  
par  
pid  
st   
371  alias is_O_with_neg_right ↔ asymptotics.is_O_with.of_neg_right asymptotics.is_O_with.neg_right
372  
373  @[simp] theorem is_O_neg_right : is_O f (λ x, -(g' x)) l ↔ is_O f g' l :=
id                                    └──┘        └┘      └──┘  └┘ 
src                                   └──┘                    └──┘
typ                                   └──┘        └┘      └──┘  └┘ 
doc    └──┘                           └──┘                      └──┘
374  exists_congr $ λ _, is_O_with_neg_right
id   └──────────┘       └─────────────────┘
src  └──────────┘        └─────────────────┘
typ  └──────────┘       └─────────────────┘
375  
376  alias is_O_neg_right ↔ asymptotics.is_O.of_neg_right asymptotics.is_O.neg_right
377  
378  @[simp] theorem is_o_neg_right : is_o f (λ x, -(g' x)) l ↔ is_o f g' l :=
id                                    └──┘        └┘      └──┘  └┘ 
src                                   └──┘                    └──┘
typ                                   └──┘        └┘      └──┘  └┘ 
doc    └──┘                           └──┘                      └──┘
379  forall_congr $ λ _, forall_congr $ λ _, is_O_with_neg_right
id   └──────────┘       └──────────┘       └─────────────────┘
src  └──────────┘        └──────────┘        └─────────────────┘
typ  └──────────┘       └──────────┘       └─────────────────┘
380  
381  alias is_o_neg_right ↔ asymptotics.is_o.of_neg_right asymptotics.is_o.neg_right
382  
383  @[simp] theorem is_O_with_neg_left : is_O_with c (λ x, -(f' x)) g l ↔ is_O_with c f' g l :=
id                                        └───────┘        └┘       └───────┘  └┘  
src                                       └───────┘                      └───────┘
typ                                       └───────┘        └┘       └───────┘  └┘  
doc    └──┘                               └───────┘                        └───────┘
384  by simp only [is_O_with, norm_neg]
id                 └───────┘  └──────┘
src     └─────────┘└───────┘└┘└──────┘└─
typ     └─────────┘└───────┘└┘└──────┘└─
doc     └─────────┘└───────┘└┘        └─
txt     └─────────┘         └┘        └─
par     └─────────┘         └┘        └─
pid         └──┘└┘         └┘        
st     └────────────────────────────────
385  
src  
typ  
doc  
txt  
par  
pid  
st   
386  alias is_O_with_neg_left ↔ asymptotics.is_O_with.of_neg_left asymptotics.is_O_with.neg_left
387  
388  @[simp] theorem is_O_neg_left : is_O (λ x, -(f' x)) g l ↔ is_O f' g l :=
id                                   └──┘       └┘       └──┘ └┘  
src                                  └──┘                    └──┘
typ                                  └──┘       └┘       └──┘ └┘  
doc    └──┘                          └──┘                      └──┘
389  exists_congr $ λ _, is_O_with_neg_left
id   └──────────┘       └────────────────┘
src  └──────────┘        └────────────────┘
typ  └──────────┘       └────────────────┘
390  
391  alias is_O_neg_left ↔ asymptotics.is_O.of_neg_left asymptotics.is_O.neg_left
392  
393  @[simp] theorem is_o_neg_left : is_o (λ x, -(f' x)) g l ↔ is_o f' g l :=
id                                   └──┘       └┘       └──┘ └┘  
src                                  └──┘                    └──┘
typ                                  └──┘       └┘       └──┘ └┘  
doc    └──┘                          └──┘                      └──┘
394  forall_congr $ λ _, forall_congr $ λ _, is_O_with_neg_left
id   └──────────┘       └──────────┘       └────────────────┘
src  └──────────┘        └──────────┘        └────────────────┘
typ  └──────────┘       └──────────┘       └────────────────┘
395  
396  alias is_o_neg_left ↔ asymptotics.is_o.of_neg_right asymptotics.is_o.neg_left
397  
398  /-! ### Product of functions (right) -/
399  
400  lemma is_O_with_fst_prod : is_O_with 1 f' (λ x, (f' x, g' x)) l :=
id                              └───────┘   └┘      └┘   └┘    
src                             └───────┘            
typ                             └───────┘   └┘      └┘   └┘    
doc                             └───────┘
401  is_O_with_of_le l $ λ x, le_max_left _ _
id   └─────────────┘        └─────────┘
src  └─────────────┘          └─────────┘
typ  └─────────────┘        └─────────┘
402  
403  lemma is_O_with_snd_prod : is_O_with 1 g' (λ x, (f' x, g' x)) l :=
id                              └───────┘   └┘      └┘   └┘    
src                             └───────┘            
typ                             └───────┘   └┘      └┘   └┘    
doc                             └───────┘
404  is_O_with_of_le l $ λ x, le_max_right _ _
id   └─────────────┘        └──────────┘
src  └─────────────┘          └──────────┘
typ  └─────────────┘        └──────────┘
405  
406  lemma is_O_fst_prod : is_O f' (λ x, (f' x, g' x)) l := is_O_with_fst_prod.is_O
id                         └──┘ └┘      └┘   └┘        └────────────────┘└───┘
src                        └──┘                            └────────────────┘└───┘
typ                        └──┘ └┘      └┘   └┘        └────────────────┘└───┘
doc                        └──┘
407  
408  lemma is_O_snd_prod : is_O g' (λ x, (f' x, g' x)) l := is_O_with_snd_prod.is_O
id                         └──┘ └┘      └┘   └┘        └────────────────┘└───┘
src                        └──┘                            └────────────────┘└───┘
typ                        └──┘ └┘      └┘   └┘        └────────────────┘└───┘
doc                        └──┘
409  
410  section
411  
412  variables (f' k')
413  
414  lemma is_O_with.prod_rightl (h : is_O_with c f g' l) (hc : 0 ≤ c) :
id                                    └───────┘   └┘            
src                                   └───────┘                   
typ                                   └───────┘   └┘            
doc                                   └───────┘
415    is_O_with c f (λ x, (g' x, k' x)) l :=
id     └───────┘        └┘   └┘    
src    └───────┘           
typ    └───────┘        └┘   └┘    
doc    └───────┘
416  (h.trans is_O_with_fst_prod hc).congr_const (mul_one c)
id    └────┘ └────────────────┘ └┘ └─────────┘   └─────┘ 
src    └────┘ └────────────────┘    └─────────┘   └─────┘
typ   └────┘ └────────────────┘ └┘ └─────────┘   └─────┘ 
417  
418  lemma is_O.prod_rightl (h : is_O f g' l) : is_O f (λx, (g' x, k' x)) l :=
id                               └──┘  └┘     └──┘      └┘   └┘    
src                              └──┘           └──┘        
typ                              └──┘  └┘     └──┘      └┘   └┘    
doc                              └──┘           └──┘
419  let ⟨c, cnonneg, hc⟩ := h.exists_nonneg in (hc.prod_rightl k' cnonneg).is_O
id   └─┘     └─────┘  └┘     └────────────┘       └──────────┘ └┘         └──┘
src                           └────────────┘       └──────────┘            └──┘
typ  └─┘     └─────┘  └┘     └────────────┘       └──────────┘ └┘         └──┘
420  
421  lemma is_o.prod_rightl (h : is_o f g' l) : is_o f (λ x, (g' x, k' x)) l :=
id                               └──┘  └┘     └──┘       └┘   └┘    
src                              └──┘           └──┘         
typ                              └──┘  └┘     └──┘       └┘   └┘    
doc                              └──┘           └──┘
422  λ c cpos, (h cpos).prod_rightl k' (le_of_lt cpos)
id      └──┘    └──┘ └─────────┘  └┘  └──────┘ └──┘
src                    └─────────┘      └──────┘
typ     └──┘    └──┘ └─────────┘  └┘  └──────┘ └──┘
423  
424  lemma is_O_with.prod_rightr (h : is_O_with c f g' l) (hc : 0 ≤ c) :
id                                    └───────┘   └┘            
src                                   └───────┘                   
typ                                   └───────┘   └┘            
doc                                   └───────┘
425    is_O_with c f (λ x, (f' x, g' x)) l :=
id     └───────┘        └┘   └┘    
src    └───────┘           
typ    └───────┘        └┘   └┘    
doc    └───────┘
426  (h.trans is_O_with_snd_prod hc).congr_const (mul_one c)
id    └────┘ └────────────────┘ └┘ └─────────┘   └─────┘ 
src    └────┘ └────────────────┘    └─────────┘   └─────┘
typ   └────┘ └────────────────┘ └┘ └─────────┘   └─────┘ 
427  
428  lemma is_O.prod_rightr (h : is_O f g' l) : is_O f (λx, (f' x, g' x)) l :=
id                               └──┘  └┘     └──┘      └┘   └┘    
src                              └──┘           └──┘        
typ                              └──┘  └┘     └──┘      └┘   └┘    
doc                              └──┘           └──┘
429  let ⟨c, cnonneg, hc⟩ := h.exists_nonneg in (hc.prod_rightr f' cnonneg).is_O
id   └─┘     └─────┘  └┘     └────────────┘       └──────────┘ └┘         └──┘
src                           └────────────┘       └──────────┘            └──┘
typ  └─┘     └─────┘  └┘     └────────────┘       └──────────┘ └┘         └──┘
430  
431  lemma is_o.prod_rightr (h : is_o f g' l) : is_o f (λx, (f' x, g' x)) l :=
id                               └──┘  └┘     └──┘      └┘   └┘    
src                              └──┘           └──┘        
typ                              └──┘  └┘     └──┘      └┘   └┘    
doc                              └──┘           └──┘
432  λ c cpos, (h cpos).prod_rightr f' (le_of_lt cpos)
id      └──┘    └──┘ └─────────┘  └┘  └──────┘ └──┘
src                    └─────────┘      └──────┘
typ     └──┘    └──┘ └─────────┘  └┘  └──────┘ └──┘
433  
434  end
435  
436  lemma is_O_with.prod_left_same (hf : is_O_with c f' k' l) (hg : is_O_with c g' k' l) :
id                                        └───────┘  └┘ └┘         └───────┘  └┘ └┘ 
src                                       └───────┘                  └───────┘
typ                                       └───────┘  └┘ └┘         └───────┘  └┘ └┘ 
doc                                       └───────┘                  └───────┘
437    is_O_with c (λ x, (f' x, g' x)) k' l :=
id     └───────┘       └┘   └┘    └┘ 
src    └───────┘         
typ    └───────┘       └┘   └┘    └┘ 
doc    └───────┘
438  begin
st   └─────
439    filter_upwards [hf, hg],
src    └──────────────┘  └┘  
typ    └──────────────┘  └┘  
doc    └──────────────┘  └┘  
txt    └──────────────┘  └┘  
par    └──────────────┘  └┘  
pid                  └┘  └┘  
st   ────────────────────────┘└─
440    simp only [mem_set_of_eq],
id                └───────────┘
src    └─────────┘└───────────┘
typ    └─────────┘└───────────┘
doc    └─────────┘             
txt    └─────────┘             
par    └─────────┘             
pid        └──┘└┘             
st   ──────────────────────────┘└─
441    exact λ x, max_le
id                └────┘
src    └────┘ └──┘└────┘
typ    └────┘ └──┘└────┘
doc    └────┘ └──┘      
txt    └────┘ └──┘      
par    └────┘ └──┘      
pid          └──┘      
st   ───────────────────┘
442  end
st   └─┘
443  
444  lemma is_O_with.prod_left (hf : is_O_with c f' k' l) (hg : is_O_with c' g' k' l) :
id                                   └───────┘  └┘ └┘         └───────┘ └┘ └┘ └┘ 
src                                  └───────┘                  └───────┘
typ                                  └───────┘  └┘ └┘         └───────┘ └┘ └┘ └┘ 
doc                                  └───────┘                  └───────┘
445    is_O_with (max c c') (λ x, (f' x, g' x)) k' l :=
id     └───────┘  └─┘  └┘       └┘   └┘    └┘ 
src    └───────┘  └─┘             
typ    └───────┘  └─┘  └┘       └┘   └┘    └┘ 
doc    └───────┘
446  (hf.weaken $ le_max_left c c').prod_left_same (hg.weaken $ le_max_right c c')
id    └┘└─────┘   └─────────┘  └┘ └────────────┘   └┘└─────┘   └──────────┘  └┘
src     └─────┘   └─────────┘      └────────────┘     └─────┘   └──────────┘
typ   └┘└─────┘   └─────────┘  └┘ └────────────┘   └┘└─────┘   └──────────┘  └┘
447  
448  lemma is_O_with.prod_left_fst (h : is_O_with c (λ x, (f' x, g' x)) k' l) :
id                                      └───────┘       └┘   └┘    └┘ 
src                                     └───────┘         
typ                                     └───────┘       └┘   └┘    └┘ 
doc                                     └───────┘
449    is_O_with c f' k' l :=
id     └───────┘  └┘ └┘ 
src    └───────┘
typ    └───────┘  └┘ └┘ 
doc    └───────┘
450  (is_O_with_fst_prod.trans h zero_le_one).congr_const $ one_mul c
id    └────────────────┘└────┘  └─────────┘ └─────────┘    └─────┘ 
src   └────────────────┘└────┘   └─────────┘ └─────────┘    └─────┘
typ   └────────────────┘└────┘  └─────────┘ └─────────┘    └─────┘ 
451  
452  lemma is_O_with.prod_left_snd (h : is_O_with c (λ x, (f' x, g' x)) k' l) :
id                                      └───────┘       └┘   └┘    └┘ 
src                                     └───────┘         
typ                                     └───────┘       └┘   └┘    └┘ 
doc                                     └───────┘
453    is_O_with c g' k' l :=
id     └───────┘  └┘ └┘ 
src    └───────┘
typ    └───────┘  └┘ └┘ 
doc    └───────┘
454  (is_O_with_snd_prod.trans h zero_le_one).congr_const $ one_mul c
id    └────────────────┘└────┘  └─────────┘ └─────────┘    └─────┘ 
src   └────────────────┘└────┘   └─────────┘ └─────────┘    └─────┘
typ   └────────────────┘└────┘  └─────────┘ └─────────┘    └─────┘ 
455  
456  lemma is_O_with_prod_left :
457     is_O_with c (λ x, (f' x, g' x)) k' l ↔ is_O_with c f' k' l ∧ is_O_with c g' k' l :=
id      └───────┘       └┘   └┘    └┘   └───────┘  └┘ └┘   └───────┘  └┘ └┘ 
src     └───────┘                            └───────┘            └───────┘
typ     └───────┘       └┘   └┘    └┘   └───────┘  └┘ └┘   └───────┘  └┘ └┘ 
doc     └───────┘                              └───────┘             └───────┘
458  ⟨λ h, ⟨h.prod_left_fst, h.prod_left_snd⟩, λ h, h.1.prod_left_same h.2⟩
id         └────────────┘  └────────────┘        └────────────┘  
src          └────────────┘   └────────────┘          └────────────┘   
typ        └────────────┘  └────────────┘        └────────────┘  
459  
460  lemma is_O.prod_left (hf : is_O f' k' l) (hg : is_O g' k' l) : is_O (λ x, (f' x, g' x)) k' l :=
id                              └──┘ └┘ └┘         └──┘ └┘ └┘     └──┘      └┘   └┘    └┘ 
src                             └──┘                └──┘            └──┘       
typ                             └──┘ └┘ └┘         └──┘ └┘ └┘     └──┘      └┘   └┘    └┘ 
doc                             └──┘                └──┘            └──┘
461  let ⟨c, hf⟩ := hf, ⟨c', hg⟩ := hg in (hf.prod_left hg).is_O
id   └─┘     └┘     └┘       └┘     └┘       └────────┘    └──┘
src                                          └────────┘    └──┘
typ  └─┘     └┘     └┘       └┘     └┘       └────────┘    └──┘
462  
463  lemma is_O.prod_left_fst (h : is_O (λ x, (f' x, g' x)) k' l) : is_O f' k' l :=
id                                 └──┘      └┘   └┘    └┘     └──┘ └┘ └┘ 
src                                └──┘                            └──┘
typ                                └──┘      └┘   └┘    └┘     └──┘ └┘ └┘ 
doc                                └──┘                             └──┘
464  is_O_fst_prod.trans h
id   └───────────┘└────┘ 
src  └───────────┘└────┘
typ  └───────────┘└────┘ 
465  
466  lemma is_O.prod_left_snd (h : is_O (λ x, (f' x, g' x)) k' l) : is_O g' k' l :=
id                                 └──┘      └┘   └┘    └┘     └──┘ └┘ └┘ 
src                                └──┘                            └──┘
typ                                └──┘      └┘   └┘    └┘     └──┘ └┘ └┘ 
doc                                └──┘                             └──┘
467  is_O_snd_prod.trans h
id   └───────────┘└────┘ 
src  └───────────┘└────┘
typ  └───────────┘└────┘ 
468  
469  @[simp] lemma is_O_prod_left :
doc    └──┘
470    is_O (λ x, (f' x, g' x)) k' l ↔ is_O f' k' l ∧ is_O g' k' l :=
id     └──┘      └┘   └┘    └┘   └──┘ └┘ └┘   └──┘ └┘ └┘ 
src    └──┘                          └──┘          └──┘
typ    └──┘      └┘   └┘    └┘   └──┘ └┘ └┘   └──┘ └┘ └┘ 
doc    └──┘                            └──┘           └──┘
471  ⟨λ h, ⟨h.prod_left_fst, h.prod_left_snd⟩, λ h, h.1.prod_left h.2⟩
id         └────────────┘  └────────────┘        └───────┘  
src          └────────────┘   └────────────┘          └───────┘   
typ        └────────────┘  └────────────┘        └───────┘  
472  
473  lemma is_o.prod_left (hf : is_o f' k' l) (hg : is_o g' k' l) : is_o (λ x, (f' x, g' x)) k' l :=
id                              └──┘ └┘ └┘         └──┘ └┘ └┘     └──┘      └┘   └┘    └┘ 
src                             └──┘                └──┘            └──┘       
typ                             └──┘ └┘ └┘         └──┘ └┘ └┘     └──┘      └┘   └┘    └┘ 
doc                             └──┘                └──┘            └──┘
474  λ c hc, (hf hc).prod_left_same (hg hc)
id      └┘   └┘ └┘ └────────────┘   └┘ └┘
src                 └────────────┘
typ     └┘   └┘ └┘ └────────────┘   └┘ └┘
475  
476  lemma is_o.prod_left_fst (h : is_o (λ x, (f' x, g' x)) k' l) : is_o f' k' l :=
id                                 └──┘      └┘   └┘    └┘     └──┘ └┘ └┘ 
src                                └──┘                            └──┘
typ                                └──┘      └┘   └┘    └┘     └──┘ └┘ └┘ 
doc                                └──┘                             └──┘
477  is_O_fst_prod.trans_is_o h
id   └───────────┘└─────────┘ 
src  └───────────┘└─────────┘
typ  └───────────┘└─────────┘ 
478  
479  lemma is_o.prod_left_snd (h : is_o (λ x, (f' x, g' x)) k' l) : is_o g' k' l :=
id                                 └──┘      └┘   └┘    └┘     └──┘ └┘ └┘ 
src                                └──┘                            └──┘
typ                                └──┘      └┘   └┘    └┘     └──┘ └┘ └┘ 
doc                                └──┘                             └──┘
480  is_O_snd_prod.trans_is_o h
id   └───────────┘└─────────┘ 
src  └───────────┘└─────────┘
typ  └───────────┘└─────────┘ 
481  
482  @[simp] lemma is_o_prod_left :
doc    └──┘
483    is_o (λ x, (f' x, g' x)) k' l ↔ is_o f' k' l ∧ is_o g' k' l :=
id     └──┘      └┘   └┘    └┘   └──┘ └┘ └┘   └──┘ └┘ └┘ 
src    └──┘                          └──┘          └──┘
typ    └──┘      └┘   └┘    └┘   └──┘ └┘ └┘   └──┘ └┘ └┘ 
doc    └──┘                            └──┘           └──┘
484  ⟨λ h, ⟨h.prod_left_fst, h.prod_left_snd⟩, λ h, h.1.prod_left h.2⟩
id         └────────────┘  └────────────┘        └───────┘  
src          └────────────┘   └────────────┘          └───────┘   
typ        └────────────┘  └────────────┘        └───────┘  
485  
486  /-! ### Addition and subtraction -/
487  
488  section add_sub
489  
490  variables {c₁ c₂ : ℝ} {f₁ f₂ : α → E'}
id                      
src                     
typ                     
491  
492  theorem is_O_with.add (h₁ : is_O_with c₁ f₁ g l) (h₂ : is_O_with c₂ f₂ g l) :
id                               └───────┘ └┘ └┘          └───────┘ └┘ └┘  
src                              └───────┘                  └───────┘
typ                              └───────┘ └┘ └┘          └───────┘ └┘ └┘  
doc                              └───────┘                  └───────┘
493    is_O_with (c₁ + c₂) (λ x, f₁ x + f₂ x) g l :=
id     └───────┘  └┘  └┘       └┘   └┘    
src    └───────┘                     
typ    └───────┘  └┘  └┘       └┘   └┘    
doc    └───────┘
494  by filter_upwards [h₁, h₂] λ x hx₁ hx₂,
src     └──────────────┘  └┘  └┘ └──────────┘
typ     └──────────────┘  └┘  └┘ └──────────┘
doc     └──────────────┘  └┘  └┘ └──────────┘
txt     └──────────────┘  └┘  └┘ └──────────┘
par     └──────────────┘  └┘  └┘ └──────────┘
pid                   └┘  └┘   └──────────┘
st     └─────────────────────────────────────
495  calc ∥f₁ x + f₂ x∥ ≤ c₁ * ∥g x∥ + c₂ * ∥g x∥ : norm_add_le_of_le hx₁ hx₂
id        └┘    └┘                              └───────────────┘
src                           └─┘└───────────────┘      
typ      └┘ └┘                └─┘└───────────────┘      
doc                               └─┘                       
txt                               └─┘                       
par                               └─┘                       
pid                               └─┘                       
st   ─────────────────────────────────────────────────────────────────────────
496                 ... = (c₁ + c₂) * ∥g x∥       : (add_mul _ _ _).symm
id                         └┘   └┘                  └─────┘
src  ──────────────────┘       └┘     └───────┘ └─────┘└────────────
typ  ──────────────────┘  └┘ └┘└┘    └───────┘ └─────┘└────────────
doc  ──────────────────┘       └┘     └───────┘        └────────────
txt  ──────────────────┘       └┘     └───────┘        └────────────
par  ──────────────────┘       └┘     └───────┘        └────────────
pid  ──────────────────┘       └┘     └───────┘        └─────────┘└─
st   ────────────────────────────────────────────────────────────────────
497  
src  
typ  
doc  
txt  
par  
pid  
st   
498  theorem is_O.add : is_O f₁ g l → is_O f₂ g l → is_O (λ x, f₁ x + f₂ x) g l
id                      └──┘ └┘    └──┘ └┘     └──┘      └┘   └┘    
src                     └──┘          └──┘          └──┘            
typ                     └──┘ └┘    └──┘ └┘     └──┘      └┘   └┘    
doc                     └──┘          └──┘          └──┘
499  | ⟨c₁, hc₁⟩ ⟨c₂, hc₂⟩ := (hc₁.add hc₂).is_O
id          └─┘       └─┘         └──┘     └──┘
src                               └──┘     └──┘
typ         └─┘       └─┘         └──┘     └──┘
500  
501  theorem is_o.add (h₁ : is_o f₁ g l) (h₂ : is_o f₂ g l) : is_o (λ x, f₁ x + f₂ x) g l :=
id                          └──┘ └┘          └──┘ └┘      └──┘      └┘   └┘    
src                         └──┘               └──┘           └──┘            
typ                         └──┘ └┘          └──┘ └┘      └──┘      └┘   └┘    
doc                         └──┘               └──┘           └──┘
502  λ c cpos, ((h₁ $ half_pos cpos).add (h₂ $ half_pos cpos)).congr_const (add_halves c)
id      └──┘    └┘   └──────┘ └──┘ └─┘   └┘   └──────┘ └──┘  └─────────┘   └────────┘ 
src                   └──────┘      └─┘        └──────┘       └─────────┘   └────────┘
typ     └──┘    └┘   └──────┘ └──┘ └─┘   └┘   └──────┘ └──┘  └─────────┘   └────────┘ 
503  
504  theorem is_O.add_is_o (h₁ : is_O f₁ g l) (h₂ : is_o f₂ g l) : is_O (λ x, f₁ x + f₂ x) g l :=
id                               └──┘ └┘          └──┘ └┘      └──┘      └┘   └┘    
src                              └──┘               └──┘           └──┘            
typ                              └──┘ └┘          └──┘ └┘      └──┘      └┘   └┘    
doc                              └──┘               └──┘           └──┘
505  h₁.add h₂.is_O
id   └┘└──┘ └┘└───┘
src    └──┘   └───┘
typ  └┘└──┘ └┘└───┘
506  
507  theorem is_o.add_is_O (h₁ : is_o f₁ g l) (h₂ : is_O f₂ g l) : is_O (λ x, f₁ x + f₂ x) g l :=
id                               └──┘ └┘          └──┘ └┘      └──┘      └┘   └┘    
src                              └──┘               └──┘           └──┘            
typ                              └──┘ └┘          └──┘ └┘      └──┘      └┘   └┘    
doc                              └──┘               └──┘           └──┘
508  h₁.is_O.add h₂
id   └┘└───┘└──┘ └┘
src    └───┘└──┘
typ  └┘└───┘└──┘ └┘
509  
510  theorem is_O_with.add_is_o (h₁ : is_O_with c₁ f₁ g l) (h₂ : is_o f₂ g l) (hc : c₁ < c₂) :
id                                    └───────┘ └┘ └┘          └──┘ └┘          └┘  └┘
src                                   └───────┘                  └──┘                  
typ                                   └───────┘ └┘ └┘          └──┘ └┘          └┘  └┘
doc                                   └───────┘                  └──┘
511    is_O_with c₂ (λx, f₁ x + f₂ x) g l :=
id     └───────┘ └┘     └┘   └┘    
src    └───────┘              
typ    └───────┘ └┘     └┘   └┘    
doc    └───────┘
512  (h₁.add (h₂ (sub_pos.2 hc))).congr_const (add_sub_cancel'_right _ _)
id    └┘└──┘  └┘  └─────┘  └┘   └─────────┘   └───────────────────┘
src     └──┘      └─────┘       └─────────┘   └───────────────────┘
typ   └┘└──┘  └┘  └─────┘  └┘   └─────────┘   └───────────────────┘
513  
514  theorem is_o.add_is_O_with (h₁ : is_o f₁ g l) (h₂ : is_O_with c₁ f₂ g l) (hc : c₁ < c₂) :
id                                    └──┘ └┘          └───────┘ └┘ └┘          └┘  └┘
src                                   └──┘               └───────┘                     
typ                                   └──┘ └┘          └───────┘ └┘ └┘          └┘  └┘
doc                                   └──┘               └───────┘
515    is_O_with c₂ (λx, f₁ x + f₂ x) g l :=
id     └───────┘ └┘     └┘   └┘    
src    └───────┘              
typ    └───────┘ └┘     └┘   └┘    
doc    └───────┘
516  (h₂.add_is_o h₁ hc).congr_left $ λ _, add_comm _ _
id    └┘└───────┘ └┘ └┘ └────────┘        └──────┘
src     └───────┘       └────────┘         └──────┘
typ   └┘└───────┘ └┘ └┘ └────────┘        └──────┘
517  
518  theorem is_O_with.sub (h₁ : is_O_with c₁ f₁ g l) (h₂ : is_O_with c₂ f₂ g l) :
id                               └───────┘ └┘ └┘          └───────┘ └┘ └┘  
src                              └───────┘                  └───────┘
typ                              └───────┘ └┘ └┘          └───────┘ └┘ └┘  
doc                              └───────┘                  └───────┘
519    is_O_with (c₁ + c₂) (λ x, f₁ x - f₂ x) g l :=
id     └───────┘  └┘  └┘       └┘   └┘    
src    └───────┘                     
typ    └───────┘  └┘  └┘       └┘   └┘    
doc    └───────┘
520  h₁.add h₂.neg_left
id   └┘└──┘ └┘└───────┘
src    └──┘
typ  └┘└──┘ └┘└───────┘
doc           └───────┘
521  
522  theorem is_O_with.sub_is_o (h₁ : is_O_with c₁ f₁ g l) (h₂ : is_o f₂ g l) (hc : c₁ < c₂) :
id                                    └───────┘ └┘ └┘          └──┘ └┘          └┘  └┘
src                                   └───────┘                  └──┘                  
typ                                   └───────┘ └┘ └┘          └──┘ └┘          └┘  └┘
doc                                   └───────┘                  └──┘
523    is_O_with c₂ (λ x, f₁ x - f₂ x) g l :=
id     └───────┘ └┘      └┘   └┘    
src    └───────┘               
typ    └───────┘ └┘      └┘   └┘    
doc    └───────┘
524  h₁.add_is_o h₂.neg_left hc
id   └┘└───────┘ └┘└───────┘ └┘
src    └───────┘
typ  └┘└───────┘ └┘└───────┘ └┘
doc                └───────┘
525  
526  theorem is_O.sub (h₁ : is_O f₁ g l) (h₂ : is_O f₂ g l) : is_O (λ x, f₁ x - f₂ x) g l :=
id                          └──┘ └┘          └──┘ └┘      └──┘      └┘   └┘    
src                         └──┘               └──┘           └──┘            
typ                         └──┘ └┘          └──┘ └┘      └──┘      └┘   └┘    
doc                         └──┘               └──┘           └──┘
527  h₁.add h₂.neg_left
id   └┘└──┘ └┘└───────┘
src    └──┘
typ  └┘└──┘ └┘└───────┘
doc           └───────┘
528  
529  theorem is_o.sub (h₁ : is_o f₁ g l) (h₂ : is_o f₂ g l) : is_o (λ x, f₁ x - f₂ x) g l :=
id                          └──┘ └┘          └──┘ └┘      └──┘      └┘   └┘    
src                         └──┘               └──┘           └──┘            
typ                         └──┘ └┘          └──┘ └┘      └──┘      └┘   └┘    
doc                         └──┘               └──┘           └──┘
530  h₁.add h₂.neg_left
id   └┘└──┘ └┘└───────┘
src    └──┘
typ  └┘└──┘ └┘└───────┘
doc           └───────┘
531  
532  end add_sub
533  
534  /-! ### Lemmas about `is_O (f₁ - f₂) g l` / `is_o (f₁ - f₂) g l` treated as a binary relation -/
535  
536  section is_oO_as_rel
537  
538  variables {f₁ f₂ f₃ : α → E'}
539  
540  theorem is_O_with.symm (h : is_O_with c (λ x, f₁ x - f₂ x) g l) :
id                               └───────┘       └┘   └┘    
src                              └───────┘              
typ                              └───────┘       └┘   └┘    
doc                              └───────┘
541    is_O_with c (λ x, f₂ x - f₁ x) g l :=
id     └───────┘       └┘   └┘    
src    └───────┘              
typ    └───────┘       └┘   └┘    
doc    └───────┘
542  h.neg_left.congr_left $ λ x, neg_sub _ _
id   └───────┘└─────────┘       └─────┘
src            └─────────┘        └─────┘
typ  └───────┘└─────────┘       └─────┘
doc   └───────┘
543  
544  theorem is_O_with_comm :
545    is_O_with c (λ x, f₁ x - f₂ x) g l ↔ is_O_with c (λ x, f₂ x - f₁ x) g l :=
id     └───────┘       └┘   └┘      └───────┘       └┘   └┘    
src    └───────┘                          └───────┘              
typ    └───────┘       └┘   └┘      └───────┘       └┘   └┘    
doc    └───────┘                            └───────┘
546  ⟨is_O_with.symm, is_O_with.symm⟩
id    └────────────┘  └────────────┘
src   └────────────┘  └────────────┘
typ   └────────────┘  └────────────┘
547  
548  theorem is_O.symm (h : is_O (λ x, f₁ x - f₂ x) g l) : is_O (λ x, f₂ x - f₁ x) g l :=
id                          └──┘      └┘   └┘        └──┘      └┘   └┘    
src                         └──┘                          └──┘            
typ                         └──┘      └┘   └┘        └──┘      └┘   └┘    
doc                         └──┘                           └──┘
549  h.neg_left.congr_left $ λ x, neg_sub _ _
id   └───────┘└─────────┘       └─────┘
src            └─────────┘        └─────┘
typ  └───────┘└─────────┘       └─────┘
doc   └───────┘
550  
551  theorem is_O_comm : is_O (λ x, f₁ x - f₂ x) g l ↔ is_O (λ x, f₂ x - f₁ x) g l :=
id                       └──┘      └┘   └┘      └──┘      └┘   └┘    
src                      └──┘                        └──┘            
typ                      └──┘      └┘   └┘      └──┘      └┘   └┘    
doc                      └──┘                          └──┘
552  ⟨is_O.symm, is_O.symm⟩
id    └───────┘  └───────┘
src   └───────┘  └───────┘
typ   └───────┘  └───────┘
553  
554  theorem is_o.symm (h : is_o (λ x, f₁ x - f₂ x) g l) : is_o (λ x, f₂ x - f₁ x) g l :=
id                          └──┘      └┘   └┘        └──┘      └┘   └┘    
src                         └──┘                          └──┘            
typ                         └──┘      └┘   └┘        └──┘      └┘   └┘    
doc                         └──┘                           └──┘
555  by simpa only [neg_sub] using h.neg_left
id                  └─────┘        └────────┘
src     └──────────┘└─────┘└──────┘          
typ     └──────────┘└─────┘└──────┘└────────┘
doc     └──────────┘       └──────┘└────────┘
txt     └──────────┘       └──────┘          
par     └──────────┘       └──────┘          
pid          └──┘└┘       └────┘          
st     └──────────────────────────────────────
556  
src  
typ  
doc  
txt  
par  
pid  
st   
557  theorem is_o_comm : is_o (λ x, f₁ x - f₂ x) g l ↔ is_o (λ x, f₂ x - f₁ x) g l :=
id                       └──┘      └┘   └┘      └──┘      └┘   └┘    
src                      └──┘                        └──┘            
typ                      └──┘      └┘   └┘      └──┘      └┘   └┘    
doc                      └──┘                          └──┘
558  ⟨is_o.symm, is_o.symm⟩
id    └───────┘  └───────┘
src   └───────┘  └───────┘
typ   └───────┘  └───────┘
559  
560  theorem is_O_with.triangle (h₁ : is_O_with c (λ x, f₁ x - f₂ x) g l)
id                                    └───────┘       └┘   └┘    
src                                   └───────┘              
typ                                   └───────┘       └┘   └┘    
doc                                   └───────┘
561    (h₂ : is_O_with c' (λ x, f₂ x - f₃ x) g l) :
id           └───────┘ └┘      └┘   └┘    
src          └───────┘               
typ          └───────┘ └┘      └┘   └┘    
doc          └───────┘
562    is_O_with (c + c') (λ x, f₁ x - f₃ x) g l :=
id     └───────┘    └┘       └┘   └┘    
src    └───────┘                    
typ    └───────┘    └┘       └┘   └┘    
doc    └───────┘
563  (h₁.add h₂).congr_left $ λ x, sub_add_sub_cancel _ _ _
id    └┘└──┘ └┘ └────────┘        └────────────────┘
src     └──┘    └────────┘         └────────────────┘
typ   └┘└──┘ └┘ └────────┘        └────────────────┘
564  
565  theorem is_O.triangle (h₁ : is_O (λ x, f₁ x - f₂ x) g l) (h₂ : is_O (λ x, f₂ x - f₃ x) g l) :
id                               └──┘      └┘   └┘            └──┘      └┘   └┘    
src                              └──┘                              └──┘            
typ                              └──┘      └┘   └┘            └──┘      └┘   └┘    
doc                              └──┘                               └──┘
566    is_O (λ x, f₁ x - f₃ x) g l :=
id     └──┘      └┘   └┘    
src    └──┘            
typ    └──┘      └┘   └┘    
doc    └──┘
567  (h₁.add h₂).congr_left $ λ x, sub_add_sub_cancel _ _ _
id    └┘└──┘ └┘ └────────┘        └────────────────┘
src     └──┘    └────────┘         └────────────────┘
typ   └┘└──┘ └┘ └────────┘        └────────────────┘
568  
569  theorem is_o.triangle (h₁ : is_o (λ x, f₁ x - f₂ x) g l) (h₂ : is_o (λ x, f₂ x - f₃ x) g l) :
id                               └──┘      └┘   └┘            └──┘      └┘   └┘    
src                              └──┘                              └──┘            
typ                              └──┘      └┘   └┘            └──┘      └┘   └┘    
doc                              └──┘                               └──┘
570    is_o (λ x, f₁ x - f₃ x) g l :=
id     └──┘      └┘   └┘    
src    └──┘            
typ    └──┘      └┘   └┘    
doc    └──┘
571  (h₁.add h₂).congr_left $ λ x, sub_add_sub_cancel _ _ _
id    └┘└──┘ └┘ └────────┘        └────────────────┘
src     └──┘    └────────┘         └────────────────┘
typ   └┘└──┘ └┘ └────────┘        └────────────────┘
572  
573  theorem is_O.congr_of_sub (h : is_O (λ x, f₁ x - f₂ x) g l) :
id                                  └──┘      └┘   └┘    
src                                 └──┘            
typ                                 └──┘      └┘   └┘    
doc                                 └──┘
574    is_O f₁ g l ↔ is_O f₂ g l :=
id     └──┘ └┘    └──┘ └┘  
src    └──┘         └──┘
typ    └──┘ └┘    └──┘ └┘  
doc    └──┘          └──┘
575  ⟨λ h', (h'.sub h).congr_left (λ x, sub_sub_cancel _ _),
id      └┘   └┘└──┘  └────────┘       └────────────┘
src            └──┘   └────────┘        └────────────┘
typ     └┘   └┘└──┘  └────────┘       └────────────┘
576   λ h', (h.add h').congr_left (λ x, sub_add_cancel _ _)⟩
id      └┘   └──┘ └┘ └────────┘       └────────────┘
src           └──┘    └────────┘        └────────────┘
typ     └┘   └──┘ └┘ └────────┘       └────────────┘
577  
578  theorem is_o.congr_of_sub (h : is_o (λ x, f₁ x - f₂ x) g l) :
id                                  └──┘      └┘   └┘    
src                                 └──┘            
typ                                 └──┘      └┘   └┘    
doc                                 └──┘
579    is_o f₁ g l ↔ is_o f₂ g l :=
id     └──┘ └┘    └──┘ └┘  
src    └──┘         └──┘
typ    └──┘ └┘    └──┘ └┘  
doc    └──┘          └──┘
580  ⟨λ h', (h'.sub h).congr_left (λ x, sub_sub_cancel _ _),
id      └┘   └┘└──┘  └────────┘       └────────────┘
src            └──┘   └────────┘        └────────────┘
typ     └┘   └┘└──┘  └────────┘       └────────────┘
581   λ h', (h.add h').congr_left (λ x, sub_add_cancel _ _)⟩
id      └┘   └──┘ └┘ └────────┘       └────────────┘
src           └──┘    └────────┘        └────────────┘
typ     └┘   └──┘ └┘ └────────┘       └────────────┘
582  
583  end is_oO_as_rel
584  
585  /-! ### Zero, one, and other constants -/
586  
587  section zero_const
588  
589  variables (g' l)
590  
591  theorem is_o_zero : is_o (λ x, (0 : E')) g' l :=
id                       └──┘           └┘   └┘ 
src                      └──┘
typ                      └──┘           └┘   └┘ 
doc                      └──┘
592  λ c hc, univ_mem_sets' $ λ x, by simpa using mul_nonneg (le_of_lt hc) (norm_nonneg $ g' x)
id      └┘  └────────────┘                      └────────┘  └──────┘ └┘   └─────────┘   └┘ 
src          └────────────┘           └──────────┘└────────┘ └──────┘  └┘ └─────────┘    └─
typ     └┘  └────────────┘          └──────────┘└────────┘ └──────┘└┘└┘ └─────────┘ └┘└─
doc                                   └──────────┘                     └┘                └─
txt                                   └──────────┘                     └┘                └─
par                                   └──────────┘                     └┘                └─
pid                                        └────┘                     └┘                
st                                   └──────────────────────────────────────────────────────────
593  
src  
typ  
doc  
txt  
par  
pid  
st   
594  theorem is_O_with_zero (hc : 0 < c) : is_O_with c (λ x, (0 : E')) g' l :=
id                                       └───────┘            └┘   └┘ 
src                                       └───────┘
typ                                      └───────┘            └┘   └┘ 
doc                                        └───────┘
595  (is_o_zero g' l) hc
id    └───────┘ └┘   └┘
src   └───────┘
typ   └───────┘ └┘   └┘
596  
597  theorem is_O_zero : is_O (λ x, (0 : E')) g' l := (is_o_zero g' l).is_O
id                       └──┘           └┘   └┘      └───────┘ └┘  └──┘
src                      └──┘                          └───────┘      └──┘
typ                      └──┘           └┘   └┘      └───────┘ └┘  └──┘
doc                      └──┘
598  
599  theorem is_O_refl_left : is_O (λ x, f' x - f' x) g' l :=
id                            └──┘      └┘   └┘   └┘ 
src                           └──┘            
typ                           └──┘      └┘   └┘   └┘ 
doc                           └──┘
600  (is_O_zero g' l).congr_left $ λ x, (sub_self _).symm
id    └───────┘ └┘  └────────┘         └──────┘   └──┘
src   └───────┘      └────────┘          └──────┘   └──┘
typ   └───────┘ └┘  └────────┘         └──────┘   └──┘
601  
602  theorem is_o_refl_left : is_o (λ x, f' x - f' x) g' l :=
id                            └──┘      └┘   └┘   └┘ 
src                           └──┘            
typ                           └──┘      └┘   └┘   └┘ 
doc                           └──┘
603  (is_o_zero g' l).congr_left $ λ x, (sub_self _).symm
id    └───────┘ └┘  └────────┘         └──────┘   └──┘
src   └───────┘      └────────┘          └──────┘   └──┘
typ   └───────┘ └┘  └────────┘         └──────┘   └──┘
604  
605  variables {g' l}
606  
607  theorem is_O_with_zero_right_iff :
608    is_O_with c f' (λ x, (0 : F')) l ↔ ∀ᶠ x in l, f' x = 0 :=
id     └───────┘  └┘           └┘     └┘  └┘  └┘  
src    └───────┘                         └┘   └┘        
typ    └───────┘  └┘           └┘     └┘  └┘  └┘  
doc    └───────┘                          └┘   └┘  
609  by simp only [is_O_with, exists_prop, true_and, norm_zero, mul_zero, norm_le_zero_iff]
id                 └───────┘  └─────────┘  └──────┘  └───────┘  └──────┘  └──────────────┘
src     └─────────┘└───────┘└┘└─────────┘└┘└──────┘└┘└───────┘└┘└──────┘└┘└──────────────┘└─
typ     └─────────┘└───────┘└┘└─────────┘└┘└──────┘└┘└───────┘└┘└──────┘└┘└──────────────┘└─
doc     └─────────┘└───────┘└┘           └┘        └┘         └┘        └┘                └─
txt     └─────────┘         └┘           └┘        └┘         └┘        └┘                └─
par     └─────────┘         └┘           └┘        └┘         └┘        └┘                └─
pid         └──┘└┘         └┘           └┘        └┘         └┘        └┘                
st     └────────────────────────────────────────────────────────────────────────────────────
610  
src  
typ  
doc  
txt  
par  
pid  
st   
611  theorem is_O_zero_right_iff : is_O f' (λ x, (0 : F')) l ↔ ∀ᶠ x in l, f' x = 0 :=
id                                 └──┘ └┘           └┘     └┘  └┘  └┘  
src                                └──┘                       └┘   └┘        
typ                                └──┘ └┘           └┘     └┘  └┘  └┘  
doc                                └──┘                        └┘   └┘  
612  ⟨λ h, let ⟨c, hc⟩ := h in  (is_O_with_zero_right_iff).1 hc,
id        └─┘     └┘           └──────────────────────┘ 
src                              └──────────────────────┘ 
typ       └─┘     └┘           └──────────────────────┘ 
613    λ h, (is_O_with_zero_right_iff.2 h : is_O_with 1 _ _ _).is_O⟩
id          └──────────────────────┘     └───────┘         └──┘
src          └──────────────────────┘      └───────┘         └──┘
typ         └──────────────────────┘     └───────┘         └──┘
doc                                         └───────┘
614  
615  theorem is_o_zero_right_iff :
616    is_o f' (λ x, (0 : F')) l ↔ ∀ᶠ x in l, f' x = 0 :=
id     └──┘ └┘           └┘     └┘  └┘  └┘  
src    └──┘                       └┘   └┘        
typ    └──┘ └┘           └┘     └┘  └┘  └┘  
doc    └──┘                        └┘   └┘  
617  ⟨λ h, is_O_zero_right_iff.1 h.is_O,
id        └─────────────────┘  └───┘
src        └─────────────────┘   └───┘
typ       └─────────────────┘  └───┘
618    λ h c hc, is_O_with_zero_right_iff.2 h⟩
id         └┘  └──────────────────────┘  
src              └──────────────────────┘
typ        └┘  └──────────────────────┘  
619  
620  theorem is_O_with_const_const (c : E) {c' : F'} (hc' : c' ≠ 0) (l : filter α) :
id                                              └┘         └┘          └────┘ 
src                                                                     └────┘
typ                                             └┘         └┘          └────┘ 
621    is_O_with (∥c∥ / ∥c'∥) (λ x : α, c) (λ x, c') l :=
id     └───────┘    └┘                  └┘  
src    └───────┘       
typ    └───────┘    └┘                  └┘  
doc    └───────┘
622  begin
st   └─────
623    apply univ_mem_sets',
id           └────────────┘
src    └────┘└────────────┘
typ    └────┘└────────────┘
doc    └────┘
txt    └────┘
par    └────┘
pid         
st   ─────────────────────┘└─
624    intro x,
src    └─────┘
typ    └─────┘
doc    └─────┘
txt    └─────┘
par    └─────┘
pid         └┘
st   ────────┘└─
625    rw [mem_set_of_eq, div_mul_cancel],
id         └───────────┘  └────────────┘
src    └──┘└───────────┘└┘└────────────┘
typ    └──┘└───────────┘└┘└────────────┘
doc    └──┘             └┘              
txt    └──┘             └┘              
par    └──┘             └┘              
pid      └┘             └┘              
st   ──────────────────┘└──────────────┘└──
626    rwa [ne.def, norm_eq_zero]
id          └────┘  └──────────┘
src    └───┘└────┘└┘└──────────┘└┘
typ    └───┘└────┘└┘└──────────┘└┘
doc    └───┘      └┘            └┘
txt    └───┘      └┘            └┘
par    └───┘      └┘            └┘
pid       └┘      └┘            
st   ────────────┘└────────────┘
627  end
st   └─┘
628  
629  theorem is_O_const_const (c : E) {c' : F'} (hc' : c' ≠ 0) (l : filter α) :
id                                         └┘         └┘          └────┘ 
src                                                                └────┘
typ                                        └┘         └┘          └────┘ 
630    is_O (λ x : α, c) (λ x, c') l :=
id     └──┘                 └┘  
src    └──┘
typ    └──┘                 └┘  
doc    └──┘
631  (is_O_with_const_const c hc' l).is_O
id    └───────────────────┘  └─┘  └──┘
src   └───────────────────┘         └──┘
typ   └───────────────────┘  └─┘  └──┘
632  
633  end zero_const
634  
635  theorem is_O_with_const_one (c : E) (l : filter α) : is_O_with ∥c∥ (λ x : α, c) (λ x, (1 : 𝕜)) l :=
id                                           └────┘     └───────┘                          
src                                           └────┘      └───────┘  
typ                                          └────┘     └───────┘                          
doc                                                       └───────┘
636  begin
st   └─────
637    refine (is_O_with_const_const c _ l).congr_const _,
id             └───────────────────┘    
src    └─────┘ └───────────────────┘ └─┘ └─────────────┘
typ    └─────┘ └───────────────────┘└─┘└─────────────┘
doc    └─────┘                       └─┘ └─────────────┘
txt    └─────┘                       └─┘ └─────────────┘
par    └─────┘                       └─┘ └─────────────┘
pid                                 └─┘ └─────────────┘
st   ───────────────────────────────────────────────────┘└─
638    { rw [normed_field.norm_one, div_one] },
id           └───────────────────┘  └─────┘
src      └──┘└───────────────────┘└┘└─────┘└┘
typ      └──┘└───────────────────┘└┘└─────┘└┘
doc      └──┘                     └┘       └┘
txt      └──┘                     └┘       └┘
par      └──┘                     └┘       └┘
pid        └┘                     └┘       
st   ───┘└───────────────────────┘└───────┘└┘
639    { exact one_ne_zero }
id             └─────────┘
src      └────┘└─────────┘
typ      └────┘└─────────┘
doc      └────┘           
txt      └────┘           
par      └────┘           
pid                      
st   ─────────────────────┘└─
640  end
st   ──┘
641  
642  theorem is_O_const_one (c : E) (l : filter α) : is_O (λ x : α, c) (λ x, (1 : 𝕜)) l :=
id                                      └────┘     └──┘                         
src                                      └────┘      └──┘
typ                                     └────┘     └──┘                         
doc                                                  └──┘
643  (is_O_with_const_one c l).is_O
id    └─────────────────┘   └──┘
src   └─────────────────┘     └──┘
typ   └─────────────────┘   └──┘
644  
645  section
646  
647  variable (𝕜)
648  
649  theorem is_o_const_iff_is_o_one {c : F'} (hc : c ≠ 0) :
id                                        └┘         
src                                                   
typ                                       └┘         
650    is_o f (λ x, c) l ↔ is_o f (λ x, (1:𝕜)) l :=
id     └──┘           └──┘             
src    └──┘               └──┘
typ    └──┘           └──┘             
doc    └──┘                └──┘
651  ⟨λ h, h.trans_is_O $ is_O_const_one c l, λ h, h.trans_is_O $ is_O_const_const _ hc _⟩
id        └─────────┘   └────────────┘        └─────────┘   └──────────────┘   └┘
src         └─────────┘   └────────────┘            └─────────┘   └──────────────┘
typ       └─────────┘   └────────────┘        └─────────┘   └──────────────┘   └┘
652  
653  end
654  
655  theorem is_o_const_iff {c : F'} (hc : c ≠ 0) :
id                               └┘         
src                                          
typ                              └┘         
656    is_o f' (λ x, c) l ↔ tendsto f' l (𝓝 0) :=
id     └──┘ └┘          └─────┘ └┘   
src    └──┘                └─────┘       
typ    └──┘ └┘          └─────┘ └┘   
doc    └──┘                 └─────┘       
657  (is_o_const_iff_is_o_one ℝ hc).trans
id    └─────────────────────┘  └┘ └───┘
src   └─────────────────────┘     └───┘
typ   └─────────────────────┘  └┘ └───┘
658  begin
st   └─────
659    clear hc c,
src    └────────┘
typ    └────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid         └───┘
st   ───────────┘└─
660    simp only [is_o, is_O_with, normed_field.norm_one, mul_one, normed_group.tendsto_nhds_zero],
id                └──┘  └───────┘  └───────────────────┘  └─────┘  └────────────────────────────┘
src    └─────────┘└──┘└┘└───────┘└┘└───────────────────┘└┘└─────┘└┘└────────────────────────────┘
typ    └─────────┘└──┘└┘└───────┘└┘└───────────────────┘└┘└─────┘└┘└────────────────────────────┘
doc    └─────────┘└──┘└┘└───────┘└┘                     └┘       └┘                              
txt    └─────────┘    └┘         └┘                     └┘       └┘                              
par    └─────────┘    └┘         └┘                     └┘       └┘                              
pid        └──┘└┘    └┘         └┘                     └┘       └┘                              
st   ────────────────────────────────────────────────────────────────────────────────────────────┘└─
661    -- Now the only difference is `≤` vs `<`
st   ───────────────────────────────────────────
662    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
663    { intros h ε hε0,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid            └──────┘
st   ───┘└────────────┘└─
664      apply mem_sets_of_superset (h (half_pos hε0)),
id             └──────────────────┘    └──────┘ └─┘
src      └────┘└──────────────────┘   └──────┘   └┘
typ      └────┘└──────────────────┘  └──────┘└─┘└┘
doc      └────┘                                  └┘
txt      └────┘                                  └┘
par      └────┘                                  └┘
pid                                             └┘
st   ────────────────────────────────────────────────┘└─
665      intros x hx,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid            └───┘
st   ──────────────┘└─
666      simp only [mem_set_of_eq] at hx ⊢,
id                  └───────────┘
src      └─────────┘└───────────┘└───────┘
typ      └─────────┘└───────────┘└───────┘
doc      └─────────┘             └───────┘
txt      └─────────┘             └───────┘
par      └─────────┘             └───────┘
pid          └──┘└┘             └─────┘
st   ────────────────────────────────────┘└─
667      exact lt_of_le_of_lt hx (half_lt_self hε0) },
id             └────────────┘ └┘  └──────────┘ └─┘
src      └────┘└────────────┘   └──────────┘   └┘
typ      └────┘└────────────┘└┘ └──────────┘└─┘└┘
doc      └────┘                                └┘
txt      └────┘                                └┘
par      └────┘                                └┘
pid                                           
st   ──────────────────────────────────────────────┘└┘
668    { intros h ε hε0,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid            └──────┘
st   ─────────────────┘└─
669      apply mem_sets_of_superset (h ε hε0),
id             └──────────────────┘    └─┘
src      └────┘└──────────────────┘      
typ      └────┘└──────────────────┘ └─┘
doc      └────┘                          
txt      └────┘                          
par      └────┘                          
pid                                     
st   ───────────────────────────────────────┘└─
670      intros x hx,
src      └─────────┘
typ      └─────────┘
doc      └─────────┘
txt      └─────────┘
par      └─────────┘
pid            └───┘
st   ──────────────┘└─
671      simp only [mem_set_of_eq] at hx ⊢,
id                  └───────────┘
src      └─────────┘└───────────┘└───────┘
typ      └─────────┘└───────────┘└───────┘
doc      └─────────┘             └───────┘
txt      └─────────┘             └───────┘
par      └─────────┘             └───────┘
pid          └──┘└┘             └─────┘
st   ────────────────────────────────────┘└─
672      exact le_of_lt hx }
id             └──────┘ └┘
src      └────┘└──────┘  
typ      └────┘└──────┘└┘
doc      └────┘          
txt      └────┘          
par      └────┘          
pid                     
st   ─────────────────────┘└─
673  end
st   ──┘
674  
675  theorem is_O_const_of_tendsto {y : E'} (h : tendsto f' l (𝓝 y)) {c : F'} (hc : c ≠ 0) :
id                                      └┘       └─────┘ └┘            └┘         
src                                              └─────┘                             
typ                                     └┘       └─────┘ └┘            └┘         
doc                                              └─────┘       
676    is_O f' (λ x, c) l :=
id     └──┘ └┘        
src    └──┘
typ    └──┘ └┘        
doc    └──┘
677  begin
st   └─────
678    refine is_O.trans _ (is_O_const_const (∥y∥ + 1) hc l),
id            └────────┘    └──────────────┘       └┘ 
src    └─────┘└────────┘└─┘ └──────────────┘  └──┘   
typ    └─────┘└────────┘└─┘ └──────────────┘ └──┘└┘
doc    └─────┘          └─┘                      └──┘   
txt    └─────┘          └─┘                      └──┘   
par    └─────┘          └─┘                      └──┘   
pid                    └─┘                      └──┘   
st   ──────────────────────────────────────────────────────┘└─
679    use 1,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid       
st   ──────┘└─
680    simp only [is_O_with, one_mul],
id                └───────┘  └─────┘
src    └─────────┘└───────┘└┘└─────┘
typ    └─────────┘└───────┘└┘└─────┘
doc    └─────────┘└───────┘└┘       
txt    └─────────┘         └┘       
par    └─────────┘         └┘       
pid        └──┘└┘         └┘       
st   ───────────────────────────────┘└─
681    have : tendsto (λx, ∥f' x∥) l (𝓝 ∥y∥), from (continuous_norm.tendsto _).comp h,
id            └─────┘       └┘                   └─────────────────────┘         
src    └─────┘└─────┘  └─┘     └┘       └───┘ └─────────────────────┘└───────┘
typ    └─────┘└─────┘  └─┘ └┘  └┘     └───┘ └─────────────────────┘└───────┘
doc    └─────┘└─────┘  └─┘     └┘       └───┘                        └───────┘
txt    └─────┘         └─┘     └┘        └───┘                        └───────┘
par    └─────┘         └─┘     └┘        └───┘                        └───────┘
pid    └───┘└┘         └─┘     └┘        └───┘                        └───────┘
st   ──────────────────────────────────────┘└───────────────────────────────────────┘└─
682    have Iy : ∥y∥ < ∥∥y∥ + 1∥, from lt_of_lt_of_le (lt_add_one _) (le_abs_self _),
id                                   └────────────┘  └────────┘     └─────────┘
src    └────────┘        └┘   └───┘└────────────┘ └────────┘└──┘ └─────────┘└─┘
typ    └────────┘       └┘   └───┘└────────────┘ └────────┘└──┘ └─────────┘└─┘
doc    └────────┘         └┘   └───┘                         └──┘            └─┘
txt    └────────┘         └┘   └───┘                         └──┘            └─┘
par    └────────┘         └┘   └───┘                         └──┘            └─┘
pid    └─────┘└─┘         └┘   └───┘                         └──┘            └─┘
st   ──────────────────────────┘└──────────────────────────────────────────────────┘└─
683    exact this (ge_mem_nhds Iy)
id           └──┘  └─────────┘ └┘
src    └────┘     └─────────┘  └┘
typ    └────┘└──┘ └─────────┘└┘└┘
doc    └────┘                  └┘
txt    └────┘                  └┘
par    └────┘                  └┘
pid                           
st   ─────────────────────────────┘
684  end
st   └─┘
685  
686  section
687  
688  variable (𝕜)
689  
690  theorem is_o_one_iff : is_o f' (λ x, (1 : 𝕜)) l ↔ tendsto f' l (𝓝 0) :=
id                          └──┘ └┘                └─────┘ └┘   
src                         └──┘                      └─────┘       
typ                         └──┘ └┘                └─────┘ └┘   
doc                         └──┘                       └─────┘       
691  is_o_const_iff one_ne_zero
id   └────────────┘ └─────────┘
src  └────────────┘ └─────────┘
typ  └────────────┘ └─────────┘
692  
693  theorem is_O_one_of_tendsto {y : E'} (h : tendsto f' l (𝓝 y)) :
id                                    └┘       └─────┘ └┘    
src                                            └─────┘       
typ                                   └┘       └─────┘ └┘    
doc                                            └─────┘       
694    is_O f' (λ x, (1:𝕜)) l :=
id     └──┘ └┘            
src    └──┘
typ    └──┘ └┘            
doc    └──┘
695  is_O_const_of_tendsto h one_ne_zero
id   └───────────────────┘  └─────────┘
src  └───────────────────┘   └─────────┘
typ  └───────────────────┘  └─────────┘
696  
697  theorem is_O.trans_tendsto_nhds (hfg : is_O f g' l) {y : F'} (hg : tendsto g' l (𝓝 y)) :
id                                          └──┘  └┘        └┘        └─────┘ └┘    
src                                         └──┘                        └─────┘       
typ                                         └──┘  └┘        └┘        └─────┘ └┘    
doc                                         └──┘                        └─────┘       
698    is_O f (λ x, (1:𝕜)) l :=
id     └──┘             
src    └──┘
typ    └──┘             
doc    └──┘
699  hfg.trans $ is_O_one_of_tendsto 𝕜 hg
id   └─┘└────┘   └─────────────────┘  └┘
src     └────┘   └─────────────────┘
typ  └─┘└────┘   └─────────────────┘  └┘
700  
701  end
702  
703  theorem is_O.trans_tendsto (hfg : is_O f' g' l) (hg : tendsto g' l (𝓝 0)) :
id                                     └──┘ └┘ └┘         └─────┘ └┘   
src                                    └──┘                └─────┘       
typ                                    └──┘ └┘ └┘         └─────┘ └┘   
doc                                    └──┘                └─────┘       
704    tendsto f' l (𝓝 0) :=
id     └─────┘ └┘   
src    └─────┘       
typ    └─────┘ └┘   
doc    └─────┘       
705  (is_o_one_iff ℝ).1 $ hfg.trans_is_o $ (is_o_one_iff ℝ).2 hg
id    └──────────┘      └─┘└─────────┘    └──────────┘    └┘
src   └──────────┘         └─────────┘    └──────────┘  
typ   └──────────┘      └─┘└─────────┘    └──────────┘    └┘
706  
707  theorem is_o.trans_tendsto (hfg : is_o f' g' l) (hg : tendsto g' l (𝓝 0)) :
id                                     └──┘ └┘ └┘         └─────┘ └┘   
src                                    └──┘                └─────┘       
typ                                    └──┘ └┘ └┘         └─────┘ └┘   
doc                                    └──┘                └─────┘       
708    tendsto f' l (𝓝 0) :=
id     └─────┘ └┘   
src    └─────┘       
typ    └─────┘ └┘   
doc    └─────┘       
709  hfg.is_O.trans_tendsto hg
id   └─┘└───┘└────────────┘ └┘
src     └───┘└────────────┘
typ  └─┘└───┘└────────────┘ └┘
710  
711  /-! ### Multiplication by a constant -/
712  
713  theorem is_O_with_const_mul_self (c : R) (f : α → R) (l : filter α) :
id                                                          └────┘ 
src                                                            └────┘
typ                                                         └────┘ 
714    is_O_with ∥c∥ (λ x, c * f x) f l :=
id     └───────┘             
src    └───────┘           
typ    └───────┘             
doc    └───────┘
715  is_O_with_of_le' _ $ λ x, norm_mul_le _ _
id   └──────────────┘         └─────────┘
src  └──────────────┘          └─────────┘
typ  └──────────────┘         └─────────┘
716  
717  theorem is_O_const_mul_self (c : R) (f : α → R) (l : filter α) :
id                                                     └────┘ 
src                                                       └────┘
typ                                                    └────┘ 
718    is_O (λ x, c * f x) f l :=
id     └──┘            
src    └──┘         
typ    └──┘            
doc    └──┘
719  (is_O_with_const_mul_self c f l).is_O
id    └──────────────────────┘    └──┘
src   └──────────────────────┘       └──┘
typ   └──────────────────────┘    └──┘
720  
721  theorem is_O_with.const_mul_left {f : α → R} (h : is_O_with c f g l) (c' : R) :
id                                                   └───────┘            
src                                                    └───────┘
typ                                                  └───────┘            
doc                                                    └───────┘
722    is_O_with (∥c'∥ * c) (λ x, c' * f x) g l :=
id     └───────┘  └┘         └┘      
src    └───────┘                  
typ    └───────┘  └┘         └┘      
doc    └───────┘
723  (is_O_with_const_mul_self c' f l).trans h (norm_nonneg c')
id    └──────────────────────┘ └┘   └───┘    └─────────┘ └┘
src   └──────────────────────┘        └───┘     └─────────┘
typ   └──────────────────────┘ └┘   └───┘    └─────────┘ └┘
724  
725  theorem is_O.const_mul_left {f : α → R} (h : is_O f g l) (c' : R) :
id                                              └──┘           
src                                               └──┘
typ                                             └──┘           
doc                                               └──┘
726    is_O (λ x, c' * f x) g l :=
id     └──┘      └┘      
src    └──┘          
typ    └──┘      └┘      
doc    └──┘
727  let ⟨c, hc⟩ := h in (hc.const_mul_left c').is_O
id   └─┘     └┘            └─────────────┘ └┘ └──┘
src                         └─────────────┘    └──┘
typ  └─┘     └┘            └─────────────┘ └┘ └──┘
728  
729  theorem is_O_with_self_const_mul' (u : units R) (f : α → R) (l : filter α) :
id                                          └───┘                  └────┘ 
src                                         └───┘                     └────┘
typ                                         └───┘                  └────┘ 
730    is_O_with ∥(↑u⁻¹:R)∥ f (λ x, ↑u * f x) l :=
id     └───────┘  └┘              
src    └───────┘   └┘              
typ    └───────┘  └┘              
doc    └───────┘
731  (is_O_with_const_mul_self ↑u⁻¹ _ l).congr_left $ λ x, u.inv_mul_cancel_left (f x)
id    └──────────────────────┘ └┘    └────────┘        └──────────────────┘   
src   └──────────────────────┘  └┘     └────────┘          └──────────────────┘
typ   └──────────────────────┘ └┘    └────────┘        └──────────────────┘   
732  
733  theorem is_O_with_self_const_mul (c : 𝕜) (hc : c ≠ 0) (f : α → 𝕜) (l : filter α) :
id                                                                     └────┘ 
src                                                                        └────┘
typ                                                                    └────┘ 
734    is_O_with ∥c∥⁻¹ f (λ x, c * f x) l :=
id     └───────┘ └┘            
src    └───────┘  └┘           
typ    └───────┘ └┘            
doc    └───────┘
735  (is_O_with_self_const_mul' (units.mk0 c hc) f l).congr_const $
id    └───────────────────────┘  └───────┘  └┘    └─────────┘
src   └───────────────────────┘  └───────┘           └─────────┘
typ   └───────────────────────┘  └───────┘  └┘    └─────────┘
doc                              └───────┘
736    normed_field.norm_inv c
id     └───────────────────┘ 
src    └───────────────────┘
typ    └───────────────────┘ 
737  
738  theorem is_O_self_const_mul' {c : R} (hc : is_unit c) (f : α → R) (l : filter α) :
id                                             └─────┘                  └────┘ 
src                                             └─────┘                     └────┘
typ                                            └─────┘                  └────┘ 
doc                                             └─────┘
739    is_O f (λ x, c * f x) l :=
id     └──┘            
src    └──┘           
typ    └──┘            
doc    └──┘
740  let ⟨u, hu⟩ := hc in hu.symm ▸ (is_O_with_self_const_mul' u f l).is_O
id   └─┘    └┘     └┘      └───┘   └───────────────────────┘     └──┘
src                         └───┘   └───────────────────────┘       └──┘
typ  └─┘    └┘     └┘      └───┘   └───────────────────────┘     └──┘
741  
742  theorem is_O_self_const_mul (c : 𝕜) (hc : c ≠ 0) (f : α → 𝕜) (l : filter α) :
id                                                                └────┘ 
src                                                                   └────┘
typ                                                               └────┘ 
743    is_O f (λ x, c * f x) l :=
id     └──┘            
src    └──┘           
typ    └──┘            
doc    └──┘
744  is_O_self_const_mul' (is_unit.mk0 c hc) f l
id   └──────────────────┘  └─────────┘  └┘   
src  └──────────────────┘  └─────────┘
typ  └──────────────────┘  └─────────┘  └┘   
745  
746  theorem is_O_const_mul_left_iff' {f : α → R} {c : R} (hc : is_unit c) :
id                                                           └─────┘ 
src                                                             └─────┘
typ                                                          └─────┘ 
doc                                                             └─────┘
747    is_O (λ x, c * f x) g l ↔ is_O f g l :=
id     └──┘              └──┘   
src    └──┘                    └──┘
typ    └──┘              └──┘   
doc    └──┘                      └──┘
748  ⟨(is_O_self_const_mul' hc f l).trans, λ h, h.const_mul_left c⟩
id     └──────────────────┘ └┘   └───┘       └─────────────┘ 
src    └──────────────────┘        └───┘         └─────────────┘
typ    └──────────────────┘ └┘   └───┘       └─────────────┘ 
749  
750  theorem is_O_const_mul_left_iff {f : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) :
id                                                           
src                                                              
typ                                                          
751    is_O (λ x, c * f x) g l ↔ is_O f g l :=
id     └──┘              └──┘   
src    └──┘                    └──┘
typ    └──┘              └──┘   
doc    └──┘                      └──┘
752  is_O_const_mul_left_iff' $ is_unit.mk0 c hc
id   └──────────────────────┘   └─────────┘  └┘
src  └──────────────────────┘   └─────────┘
typ  └──────────────────────┘   └─────────┘  └┘
753  
754  theorem is_o.const_mul_left {f : α → R} (h : is_o f g l) (c : R) :
id                                              └──┘          
src                                               └──┘
typ                                             └──┘          
doc                                               └──┘
755    is_o (λ x, c * f x) g l :=
id     └──┘            
src    └──┘         
typ    └──┘            
doc    └──┘
756  (is_O_const_mul_self c f l).trans_is_o h
id    └─────────────────┘    └────────┘  
src   └─────────────────┘       └────────┘
typ   └─────────────────┘    └────────┘  
757  
758  theorem is_o_const_mul_left_iff' {f : α → R} {c : R} (hc : is_unit c) :
id                                                           └─────┘ 
src                                                             └─────┘
typ                                                          └─────┘ 
doc                                                             └─────┘
759    is_o (λ x, c * f x) g l ↔ is_o f g l :=
id     └──┘              └──┘   
src    └──┘                    └──┘
typ    └──┘              └──┘   
doc    └──┘                      └──┘
760  ⟨(is_O_self_const_mul' hc f l).trans_is_o, λ h, h.const_mul_left c⟩
id     └──────────────────┘ └┘   └────────┘       └─────────────┘ 
src    └──────────────────┘        └────────┘         └─────────────┘
typ    └──────────────────┘ └┘   └────────┘       └─────────────┘ 
761  
762  theorem is_o_const_mul_left_iff {f : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) :
id                                                           
src                                                              
typ                                                          
763    is_o (λ x, c * f x) g l ↔ is_o f g l :=
id     └──┘              └──┘   
src    └──┘                    └──┘
typ    └──┘              └──┘   
doc    └──┘                      └──┘
764  is_o_const_mul_left_iff' $ is_unit.mk0 c hc
id   └──────────────────────┘   └─────────┘  └┘
src  └──────────────────────┘   └─────────┘
typ  └──────────────────────┘   └─────────┘  └┘
765  
766  theorem is_O_with.of_const_mul_right {g : α → R} {c : R} (hc' : 0 ≤ c')
id                                                                   └┘
src                                                                    
typ                                                                  └┘
767    (h : is_O_with c' f (λ x, c * g x) l) :
id          └───────┘ └┘            
src         └───────┘              
typ         └───────┘ └┘            
doc         └───────┘
768    is_O_with (c' * ∥c∥) f g l :=
id     └───────┘  └┘      
src    └───────┘       
typ    └───────┘  └┘      
doc    └───────┘
769  h.trans (is_O_with_const_mul_self c g l) hc'
id   └────┘  └──────────────────────┘     └─┘
src   └────┘  └──────────────────────┘
typ  └────┘  └──────────────────────┘     └─┘
770  
771  theorem is_O.of_const_mul_right {g : α → R} {c : R}
id                                                  
typ                                                 
772    (h : is_O f (λ x, c * g x) l) :
id          └──┘            
src         └──┘           
typ         └──┘            
doc         └──┘
773    is_O f g l :=
id     └──┘   
src    └──┘
typ    └──┘   
doc    └──┘
774  let ⟨c, cnonneg, hc⟩ := h.exists_nonneg in (hc.of_const_mul_right cnonneg).is_O
id   └─┘     └─────┘  └┘     └────────────┘       └─────────────────┘         └──┘
src                           └────────────┘       └─────────────────┘         └──┘
typ  └─┘     └─────┘  └┘     └────────────┘       └─────────────────┘         └──┘
775  
776  theorem is_O_with.const_mul_right' {g : α → R} {u : units R} {c' : ℝ} (hc' : 0 ≤ c')
id                                                     └───┘                     └┘
src                                                      └───┘                     
typ                                                    └───┘                     └┘
777    (h : is_O_with c' f g l) :
id          └───────┘ └┘   
src         └───────┘
typ         └───────┘ └┘   
doc         └───────┘
778    is_O_with (c' * ∥(↑u⁻¹:R)∥) f (λ x, ↑u * g x) l :=
id     └───────┘  └┘   └┘               
src    └───────┘        └┘               
typ    └───────┘  └┘   └┘               
doc    └───────┘
779  h.trans (is_O_with_self_const_mul' _ _ _) hc'
id   └────┘  └───────────────────────┘        └─┘
src   └────┘  └───────────────────────┘
typ  └────┘  └───────────────────────┘        └─┘
780  
781  theorem is_O_with.const_mul_right {g : α → 𝕜} {c : 𝕜} (hc : c ≠ 0)
id                                                             
src                                                                
typ                                                            
782    {c' : ℝ} (hc' : 0 ≤ c') (h : is_O_with c' f g l) :
id                       └┘       └───────┘ └┘   
src                               └───────┘
typ                      └┘       └───────┘ └┘   
doc                                 └───────┘
783    is_O_with (c' * ∥c∥⁻¹) f (λ x, c * g x) l :=
id     └───────┘  └┘  └┘             
src    └───────┘       └┘            
typ    └───────┘  └┘  └┘             
doc    └───────┘
784  h.trans (is_O_with_self_const_mul c hc g l) hc'
id   └────┘  └──────────────────────┘  └┘    └─┘
src   └────┘  └──────────────────────┘
typ  └────┘  └──────────────────────┘  └┘    └─┘
785  
786  theorem is_O.const_mul_right' {g : α → R} {c : R} (hc : is_unit c) (h : is_O f g l) :
id                                                        └─────┘        └──┘   
src                                                          └─────┘         └──┘
typ                                                       └─────┘        └──┘   
doc                                                          └─────┘         └──┘
787    is_O f (λ x, c * g x) l :=
id     └──┘            
src    └──┘           
typ    └──┘            
doc    └──┘
788  h.trans (is_O_self_const_mul' hc g l)
id   └────┘  └──────────────────┘ └┘  
src   └────┘  └──────────────────┘
typ  └────┘  └──────────────────┘ └┘  
789  
790  theorem is_O.const_mul_right {g : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) (h : is_O f g l) :
id                                                                 └──┘   
src                                                                    └──┘
typ                                                                └──┘   
doc                                                                     └──┘
791    is_O f (λ x, c * g x) l :=
id     └──┘            
src    └──┘           
typ    └──┘            
doc    └──┘
792  h.const_mul_right' $ is_unit.mk0 c hc
id   └───────────────┘   └─────────┘  └┘
src   └───────────────┘   └─────────┘
typ  └───────────────┘   └─────────┘  └┘
793  
794  theorem is_O_const_mul_right_iff' {g : α → R} {c : R} (hc : is_unit c) :
id                                                            └─────┘ 
src                                                              └─────┘
typ                                                           └─────┘ 
doc                                                              └─────┘
795    is_O f (λ x, c * g x) l ↔ is_O f g l :=
id     └──┘              └──┘   
src    └──┘                    └──┘
typ    └──┘              └──┘   
doc    └──┘                      └──┘
796  ⟨λ h, h.of_const_mul_right, λ h, h.const_mul_right' hc⟩
id        └─────────────────┘      └───────────────┘ └┘
src         └─────────────────┘        └───────────────┘
typ       └─────────────────┘      └───────────────┘ └┘
797  
798  theorem is_O_const_mul_right_iff {g : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) :
id                                                            
src                                                               
typ                                                           
799    is_O f (λ x, c * g x) l ↔ is_O f g l :=
id     └──┘              └──┘   
src    └──┘                    └──┘
typ    └──┘              └──┘   
doc    └──┘                      └──┘
800  is_O_const_mul_right_iff' $ is_unit.mk0 c hc
id   └───────────────────────┘   └─────────┘  └┘
src  └───────────────────────┘   └─────────┘
typ  └───────────────────────┘   └─────────┘  └┘
801  
802  theorem is_o.of_const_mul_right {g : α → R} {c : R} (h : is_o f (λ x, c * g x) l) :
id                                                         └──┘            
src                                                           └──┘           
typ                                                        └──┘            
doc                                                           └──┘
803    is_o f g l :=
id     └──┘   
src    └──┘
typ    └──┘   
doc    └──┘
804  h.trans_is_O (is_O_const_mul_self c g l)
id   └─────────┘  └─────────────────┘   
src   └─────────┘  └─────────────────┘
typ  └─────────┘  └─────────────────┘   
805  
806  theorem is_o.const_mul_right' {g : α → R} {c : R} (hc : is_unit c) (h : is_o f g l) :
id                                                        └─────┘        └──┘   
src                                                          └─────┘         └──┘
typ                                                       └─────┘        └──┘   
doc                                                          └─────┘         └──┘
807    is_o f (λ x, c * g x) l :=
id     └──┘            
src    └──┘           
typ    └──┘            
doc    └──┘
808  h.trans_is_O (is_O_self_const_mul' hc g l)
id   └─────────┘  └──────────────────┘ └┘  
src   └─────────┘  └──────────────────┘
typ  └─────────┘  └──────────────────┘ └┘  
809  
810  theorem is_o.const_mul_right {g : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) (h : is_o f g l) :
id                                                                 └──┘   
src                                                                    └──┘
typ                                                                └──┘   
doc                                                                     └──┘
811    is_o f (λ x, c * g x) l :=
id     └──┘            
src    └──┘           
typ    └──┘            
doc    └──┘
812  h.const_mul_right' $ is_unit.mk0 c hc
id   └───────────────┘   └─────────┘  └┘
src   └───────────────┘   └─────────┘
typ  └───────────────┘   └─────────┘  └┘
813  
814  theorem is_o_const_mul_right_iff' {g : α → R} {c : R} (hc : is_unit c) :
id                                                            └─────┘ 
src                                                              └─────┘
typ                                                           └─────┘ 
doc                                                              └─────┘
815    is_o f (λ x, c * g x) l ↔ is_o f g l :=
id     └──┘              └──┘   
src    └──┘                    └──┘
typ    └──┘              └──┘   
doc    └──┘                      └──┘
816  ⟨λ h, h.of_const_mul_right, λ h, h.const_mul_right' hc⟩
id        └─────────────────┘      └───────────────┘ └┘
src         └─────────────────┘        └───────────────┘
typ       └─────────────────┘      └───────────────┘ └┘
817  
818  theorem is_o_const_mul_right_iff {g : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) :
id                                                            
src                                                               
typ                                                           
819    is_o f (λ x, c * g x) l ↔ is_o f g l :=
id     └──┘              └──┘   
src    └──┘                    └──┘
typ    └──┘              └──┘   
doc    └──┘                      └──┘
820  is_o_const_mul_right_iff' $ is_unit.mk0 c hc
id   └───────────────────────┘   └─────────┘  └┘
src  └───────────────────────┘   └─────────┘
typ  └───────────────────────┘   └─────────┘  └┘
821  
822  /-! ### Multiplication -/
823  
824  theorem is_O_with.mul {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜} {c₁ c₂ : ℝ}
id                                                              
src                                                                 
typ                                                             
825    (h₁ : is_O_with c₁ f₁ g₁ l) (h₂ : is_O_with c₂ f₂ g₂ l) :
id           └───────┘ └┘ └┘ └┘         └───────┘ └┘ └┘ └┘ 
src          └───────┘                   └───────┘
typ          └───────┘ └┘ └┘ └┘         └───────┘ └┘ └┘ └┘ 
doc          └───────┘                   └───────┘
826    is_O_with (c₁ * c₂) (λ x, f₁ x * f₂ x) (λ x, g₁ x * g₂ x) l :=
id     └───────┘  └┘  └┘       └┘   └┘        └┘   └┘   
src    └───────┘                                       
typ    └───────┘  └┘  └┘       └┘   └┘        └┘   └┘   
doc    └───────┘
827  begin
st   └─────
828    filter_upwards [h₁, h₂], simp only [mem_set_of_eq],
id                                         └───────────┘
src    └──────────────┘  └┘    └─────────┘└───────────┘
typ    └──────────────┘  └┘    └─────────┘└───────────┘
doc    └──────────────┘  └┘    └─────────┘             
txt    └──────────────┘  └┘    └─────────┘             
par    └──────────────┘  └┘    └─────────┘             
pid                  └┘  └┘        └──┘└┘             
st   ────────────────────────┘└─────────────────────────┘└─
829    intros x hx₁ hx₂,
src    └──────────────┘
typ    └──────────────┘
doc    └──────────────┘
txt    └──────────────┘
par    └──────────────┘
pid          └────────┘
st   ─────────────────┘└─
830    apply le_trans (norm_mul_le _ _),
id           └──────┘  └─────────┘
src    └────┘└──────┘ └─────────┘└───┘
typ    └────┘└──────┘ └─────────┘└───┘
doc    └────┘                    └───┘
txt    └────┘                    └───┘
par    └────┘                    └───┘
pid                             └───┘
st   ─────────────────────────────────┘└─
831    convert mul_le_mul hx₁ hx₂ (norm_nonneg _) (le_trans (norm_nonneg _) hx₁) using 1,
id             └────────┘     └─┘                  └──────┘  └─────────┘    └─┘
src    └──────┘└────────┘                  └──┘ └──────┘ └─────────┘└──┘   └───────┘
typ    └──────┘└────────┘   └─┘            └──┘ └──────┘ └─────────┘└──┘└─┘└───────┘
doc    └──────┘                            └──┘                     └──┘   └───────┘
txt    └──────┘                            └──┘                     └──┘   └───────┘
par    └──────┘                            └──┘                     └──┘   └───────┘
pid                                       └──┘                     └──┘   └─────┘
st   ──────────────────────────────────────────────────────────────────────────────────┘└─
832    rw normed_field.norm_mul,
id        └───────────────────┘
src    └─┘└───────────────────┘
typ    └─┘└───────────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ─────────────────────────┘└─
833    ac_refl
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid           
st   ─────────┘
834  end
st   └─┘
835  
836  theorem is_O.mul {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜}
id                                              
typ                                             
837    (h₁ : is_O f₁ g₁ l) (h₂ : is_O f₂ g₂ l) :
id           └──┘ └┘ └┘         └──┘ └┘ └┘ 
src          └──┘                └──┘
typ          └──┘ └┘ └┘         └──┘ └┘ └┘ 
doc          └──┘                └──┘
838    is_O (λ x, f₁ x * f₂ x) (λ x, g₁ x * g₂ x) l :=
id     └──┘      └┘   └┘        └┘   └┘   
src    └──┘                              
typ    └──┘      └┘   └┘        └┘   └┘   
doc    └──┘
839  let ⟨c, hc⟩ := h₁, ⟨c', hc'⟩ := h₂ in (hc.mul hc').is_O
id   └─┘     └┘     └┘       └─┘     └┘       └──┘     └──┘
src                                           └──┘     └──┘
typ  └─┘     └┘     └┘       └─┘     └┘       └──┘     └──┘
840  
841  theorem is_O.mul_is_o {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜}
id                                                   
typ                                                  
842    (h₁ : is_O f₁ g₁ l) (h₂ : is_o f₂ g₂ l) :
id           └──┘ └┘ └┘         └──┘ └┘ └┘ 
src          └──┘                └──┘
typ          └──┘ └┘ └┘         └──┘ └┘ └┘ 
doc          └──┘                └──┘
843    is_o (λ x, f₁ x * f₂ x) (λ x, g₁ x * g₂ x) l :=
id     └──┘      └┘   └┘        └┘   └┘   
src    └──┘                              
typ    └──┘      └┘   └┘        └┘   └┘   
doc    └──┘
844  begin
st   └─────
845    intros c cpos,
src    └───────────┘
typ    └───────────┘
doc    └───────────┘
txt    └───────────┘
par    └───────────┘
pid          └─────┘
st   ──────────────┘└─
846    rcases h₁.exists_pos with ⟨c', c'pos, hc'⟩,
id            └───────────┘
src    └─────┘└───────────┘└────────────────────┘
typ    └─────┘└───────────┘└────────────────────┘
doc    └─────┘             └────────────────────┘
txt    └─────┘             └────────────────────┘
par    └─────┘             └────────────────────┘
pid                       └────────────────────┘
st   ───────────────────────────────────────────┘└─
847    exact (hc'.mul (h₂ (div_pos cpos c'pos))).congr_const (mul_div_cancel' _ (ne_of_gt c'pos))
id            └─────┘  └┘  └─────┘ └──┘                       └─────────────┘    └──────┘ └───┘
src    └────┘ └─────┘    └─────┘         └──────────────┘ └─────────────┘└─┘ └──────┘     └─┘
typ    └────┘ └─────┘ └┘ └─────┘└──┘     └──────────────┘ └─────────────┘└─┘ └──────┘└───┘└─┘
doc    └────┘                            └──────────────┘                └─┘              └─┘
txt    └────┘                            └──────────────┘                └─┘              └─┘
par    └────┘                            └──────────────┘                └─┘              └─┘
pid                                     └──────────────┘                └─┘              └┘
st   ────────────────────────────────────────────────────────────────────────────────────────────┘
848  end
st   └─┘
849  
850  theorem is_o.mul_is_O {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜}
id                                                   
typ                                                  
851    (h₁ : is_o f₁ g₁ l) (h₂ : is_O f₂ g₂ l) :
id           └──┘ └┘ └┘         └──┘ └┘ └┘ 
src          └──┘                └──┘
typ          └──┘ └┘ └┘         └──┘ └┘ └┘ 
doc          └──┘                └──┘
852    is_o (λ x, f₁ x * f₂ x) (λ x, g₁ x * g₂ x) l :=
id     └──┘      └┘   └┘        └┘   └┘   
src    └──┘                              
typ    └──┘      └┘   └┘        └┘   └┘   
doc    └──┘
853  begin
st   └─────
854    intros c cpos,
src    └───────────┘
typ    └───────────┘
doc    └───────────┘
txt    └───────────┘
par    └───────────┘
pid          └─────┘
st   ──────────────┘└─
855    rcases h₂.exists_pos with ⟨c', c'pos, hc'⟩,
id            └───────────┘
src    └─────┘└───────────┘└────────────────────┘
typ    └─────┘└───────────┘└────────────────────┘
doc    └─────┘             └────────────────────┘
txt    └─────┘             └────────────────────┘
par    └─────┘             └────────────────────┘
pid                       └────────────────────┘
st   ───────────────────────────────────────────┘└─
856    exact ((h₁ (div_pos cpos c'pos)).mul hc').congr_const (div_mul_cancel _ (ne_of_gt c'pos))
id             └┘  └─────┘ └──┘             └─┘               └────────────┘    └──────┘ └───┘
src    └────┘     └─────┘         └─────┘   └────────────┘ └────────────┘└─┘ └──────┘     └─┘
typ    └────┘  └┘ └─────┘└──┘     └─────┘└─┘└────────────┘ └────────────┘└─┘ └──────┘└───┘└─┘
doc    └────┘                     └─────┘   └────────────┘               └─┘              └─┘
txt    └────┘                     └─────┘   └────────────┘               └─┘              └─┘
par    └────┘                     └─────┘   └────────────┘               └─┘              └─┘
pid                              └─────┘   └────────────┘               └─┘              └┘
st   ───────────────────────────────────────────────────────────────────────────────────────────┘
857  end
st   └─┘
858  
859  theorem is_o.mul {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜} (h₁ : is_o f₁ g₁ l) (h₂ : is_o f₂ g₂ l) :
id                                                      └──┘ └┘ └┘         └──┘ └┘ └┘ 
src                                                         └──┘                └──┘
typ                                                     └──┘ └┘ └┘         └──┘ └┘ └┘ 
doc                                                         └──┘                └──┘
860    is_o (λ x, f₁ x * f₂ x) (λ x, g₁ x * g₂ x) l :=
id     └──┘      └┘   └┘        └┘   └┘   
src    └──┘                              
typ    └──┘      └┘   └┘        └┘   └┘   
doc    └──┘
861  h₁.mul_is_O h₂.is_O
id   └┘└───────┘ └┘└───┘
src    └───────┘   └───┘
typ  └┘└───────┘ └┘└───┘
862  
863  /-! ### Scalar multiplication -/
864  
865  section smul_const
866  variables [normed_space 𝕜 E']
id              └──────────┘
src             └──────────┘
typ             └──────────┘
doc             └──────────┘
867  
868  theorem is_O_with.const_smul_left (h : is_O_with c f' g l) (c' : 𝕜) :
id                                          └───────┘  └┘          
src                                         └───────┘
typ                                         └───────┘  └┘          
doc                                         └───────┘
869    is_O_with (∥c'∥ * c) (λ x, c' • f' x) g l :=
id     └───────┘  └┘         └┘  └┘    
src    └───────┘                  
typ    └───────┘  └┘         └┘  └┘    
doc    └───────┘
870  by refine ((h.norm_left.const_mul_left (∥c'∥)).congr _ _ (λ _, rfl)).of_norm_left;
id               └────────────────────────┘  └┘                   └─┘
src     └─────┘  └────────────────────────┘   └───────────┘  └──┘└─┘└─────────────┘
typ     └─────┘  └────────────────────────┘ └┘└───────────┘  └──┘└─┘└─────────────┘
doc     └─────┘  └────────────────────────┘     └───────────┘  └──┘   └─────────────┘
txt     └─────┘                                 └───────────┘  └──┘   └─────────────┘
par     └─────┘                                 └───────────┘  └──┘   └─────────────┘
pid                                            └───────────┘  └──┘   └────────────┘
st     └────────────────────────────────────────────────────────────────────────────────
871      intros; simp only [norm_norm, norm_smul]
id                          └───────┘  └───────┘
src      └────┘  └─────────┘└───────┘└┘└───────┘└─
typ      └────┘  └─────────┘└───────┘└┘└───────┘└─
doc      └────┘  └─────────┘         └┘         └─
txt      └────┘  └─────────┘         └┘         └─
par      └────┘  └─────────┘         └┘         └─
pid                  └──┘└┘         └┘         
st   ─────────────────────────────────────────────
872  
src  
typ  
doc  
txt  
par  
pid  
st   
873  theorem is_O_const_smul_left_iff {c : 𝕜} (hc : c ≠ 0) :
id                                                  
src                                                   
typ                                                 
874    is_O (λ x, c • f' x) g l ↔ is_O f' g l :=
id     └──┘        └┘      └──┘ └┘  
src    └──┘                     └──┘
typ    └──┘        └┘      └──┘ └┘  
doc    └──┘                       └──┘
875  begin
st   └─────
876    have cne0 : ∥c∥ ≠ 0, from mt (norm_eq_zero _).mp hc,
id                           └┘  └──────────┘       └┘
src    └──────────┘ └┘  └───┘└┘ └──────────┘└─────┘
typ    └──────────┘└┘  └───┘└┘ └──────────┘└─────┘└┘
doc    └──────────┘    └┘  └───┘               └─────┘
txt    └──────────┘    └┘  └───┘               └─────┘
par    └──────────┘    └┘  └───┘               └─────┘
pid    └───────┘└─┘      └───┘               └─────┘
st   ────────────────────┘└──────────────────────────────┘└─
877    rw [←is_O_norm_left], simp only [norm_smul],
id          └────────────┘              └───────┘
src    └───┘└────────────┘  └─────────┘└───────┘
typ    └───┘└────────────┘  └─────────┘└───────┘
doc    └───┘                └─────────┘         
txt    └───┘                └─────────┘         
par    └───┘                └─────────┘         
pid      └─┘                    └──┘└┘         
st   ────────────────────┘└──────────────────────┘└─
878    rw [is_O_const_mul_left_iff cne0, is_O_norm_left],
id         └─────────────────────┘ └──┘  └────────────┘
src    └──┘└─────────────────────┘    └┘└────────────┘
typ    └──┘└─────────────────────┘└──┘└┘└────────────┘
doc    └──┘                           └┘              
txt    └──┘                           └┘              
par    └──┘                           └┘              
pid      └┘                           └┘              
st   ─────────────────────────────────┘└──────────────┘└──
879  end
st   ──┘
880  
881  theorem is_o_const_smul_left (h : is_o f' g l) (c : 𝕜) :
id                                     └──┘ └┘         
src                                    └──┘
typ                                    └──┘ └┘         
doc                                    └──┘
882    is_o (λ x, c • f' x) g l :=
id     └──┘        └┘    
src    └──┘         
typ    └──┘        └┘    
doc    └──┘
883  begin
st   └─────
884    refine ((h.norm_left.const_mul_left (∥c∥)).congr_left _).of_norm_left,
id              └────────────────────────┘  
src    └─────┘  └────────────────────────┘  └───────────────────────────┘
typ    └─────┘  └────────────────────────┘ └───────────────────────────┘
doc    └─────┘  └────────────────────────┘    └───────────────────────────┘
txt    └─────┘                                └───────────────────────────┘
par    └─────┘                                └───────────────────────────┘
pid                                          └──────────────────────────┘
st   ──────────────────────────────────────────────────────────────────────┘└─
885    exact λ x, (norm_smul _ _).symm
id                 └───────┘
src    └────┘ └──┘ └───────┘└─────────┘
typ    └────┘ └──┘ └───────┘└─────────┘
doc    └────┘ └──┘          └─────────┘
txt    └────┘ └──┘          └─────────┘
par    └────┘ └──┘          └─────────┘
pid          └──┘          └───────┘└┘
st   ─────────────────────────────────┘
886  end
st   └─┘
887  
888  theorem is_o_const_smul_left_iff {c : 𝕜} (hc : c ≠ 0) :
id                                                  
src                                                   
typ                                                 
889    is_o (λ x, c • f' x) g l ↔ is_o f' g l :=
id     └──┘        └┘      └──┘ └┘  
src    └──┘                     └──┘
typ    └──┘        └┘      └──┘ └┘  
doc    └──┘                       └──┘
890  begin
st   └─────
891    have cne0 : ∥c∥ ≠ 0, from mt (norm_eq_zero _).mp hc,
id                           └┘  └──────────┘       └┘
src    └──────────┘ └┘  └───┘└┘ └──────────┘└─────┘
typ    └──────────┘└┘  └───┘└┘ └──────────┘└─────┘└┘
doc    └──────────┘    └┘  └───┘               └─────┘
txt    └──────────┘    └┘  └───┘               └─────┘
par    └──────────┘    └┘  └───┘               └─────┘
pid    └───────┘└─┘      └───┘               └─────┘
st   ────────────────────┘└──────────────────────────────┘└─
892    rw [←is_o_norm_left], simp only [norm_smul],
id          └────────────┘              └───────┘
src    └───┘└────────────┘  └─────────┘└───────┘
typ    └───┘└────────────┘  └─────────┘└───────┘
doc    └───┘                └─────────┘         
txt    └───┘                └─────────┘         
par    └───┘                └─────────┘         
pid      └─┘                    └──┘└┘         
st   ────────────────────┘└──────────────────────┘└─
893    rw [is_o_const_mul_left_iff cne0, is_o_norm_left]
id         └─────────────────────┘ └──┘  └────────────┘
src    └──┘└─────────────────────┘    └┘└────────────┘└┘
typ    └──┘└─────────────────────┘└──┘└┘└────────────┘└┘
doc    └──┘                           └┘              └┘
txt    └──┘                           └┘              └┘
par    └──┘                           └┘              └┘
pid      └┘                           └┘              
st   ─────────────────────────────────┘└──────────────┘
894  end
st   └─┘
895  
896  theorem is_O_const_smul_right {c : 𝕜} (hc : c ≠ 0) :
id                                               
src                                                
typ                                              
897    is_O f (λ x, c • f' x) l ↔ is_O f f' l :=
id     └──┘         └┘     └──┘  └┘ 
src    └──┘                     └──┘
typ    └──┘         └┘     └──┘  └┘ 
doc    └──┘                       └──┘
898  begin
st   └─────
899    have cne0 : ∥c∥ ≠ 0, from mt (norm_eq_zero _).mp hc,
id                           └┘  └──────────┘       └┘
src    └──────────┘ └┘  └───┘└┘ └──────────┘└─────┘
typ    └──────────┘└┘  └───┘└┘ └──────────┘└─────┘└┘
doc    └──────────┘    └┘  └───┘               └─────┘
txt    └──────────┘    └┘  └───┘               └─────┘
par    └──────────┘    └┘  └───┘               └─────┘
pid    └───────┘└─┘      └───┘               └─────┘
st   ────────────────────┘└──────────────────────────────┘└─
900    rw [←is_O_norm_right], simp only [norm_smul],
id          └─────────────┘              └───────┘
src    └───┘└─────────────┘  └─────────┘└───────┘
typ    └───┘└─────────────┘  └─────────┘└───────┘
doc    └───┘                 └─────────┘         
txt    └───┘                 └─────────┘         
par    └───┘                 └─────────┘         
pid      └─┘                     └──┘└┘         
st   ─────────────────────┘└──────────────────────┘└─
901    rw [is_O_const_mul_right_iff cne0, is_O_norm_right]
id         └──────────────────────┘ └──┘  └─────────────┘
src    └──┘└──────────────────────┘    └┘└─────────────┘└┘
typ    └──┘└──────────────────────┘└──┘└┘└─────────────┘└┘
doc    └──┘                            └┘               └┘
txt    └──┘                            └┘               └┘
par    └──┘                            └┘               └┘
pid      └┘                            └┘               
st   ──────────────────────────────────┘└───────────────┘
902  end
st   └─┘
903  
904  theorem is_o_const_smul_right {c : 𝕜} (hc : c ≠ 0) :
id                                               
src                                                
typ                                              
905    is_o f (λ x, c • f' x) l ↔ is_o f f' l :=
id     └──┘         └┘     └──┘  └┘ 
src    └──┘                     └──┘
typ    └──┘         └┘     └──┘  └┘ 
doc    └──┘                       └──┘
906  begin
st   └─────
907    have cne0 : ∥c∥ ≠ 0, from mt (norm_eq_zero _).mp hc,
id                           └┘  └──────────┘       └┘
src    └──────────┘ └┘  └───┘└┘ └──────────┘└─────┘
typ    └──────────┘└┘  └───┘└┘ └──────────┘└─────┘└┘
doc    └──────────┘    └┘  └───┘               └─────┘
txt    └──────────┘    └┘  └───┘               └─────┘
par    └──────────┘    └┘  └───┘               └─────┘
pid    └───────┘└─┘      └───┘               └─────┘
st   ────────────────────┘└──────────────────────────────┘└─
908    rw [←is_o_norm_right], simp only [norm_smul],
id          └─────────────┘              └───────┘
src    └───┘└─────────────┘  └─────────┘└───────┘
typ    └───┘└─────────────┘  └─────────┘└───────┘
doc    └───┘                 └─────────┘         
txt    └───┘                 └─────────┘         
par    └───┘                 └─────────┘         
pid      └─┘                     └──┘└┘         
st   ─────────────────────┘└──────────────────────┘└─
909    rw [is_o_const_mul_right_iff cne0, is_o_norm_right]
id         └──────────────────────┘ └──┘  └─────────────┘
src    └──┘└──────────────────────┘    └┘└─────────────┘└┘
typ    └──┘└──────────────────────┘└──┘└┘└─────────────┘└┘
doc    └──┘                            └┘               └┘
txt    └──┘                            └┘               └┘
par    └──┘                            └┘               └┘
pid      └┘                            └┘               
st   ──────────────────────────────────┘└───────────────┘
910  end
st   └─┘
911  
912  end smul_const
913  
914  section smul
915  
916  variables [normed_space 𝕜 E'] [normed_space 𝕜 F']
id              └──────────┘        └──────────┘
src             └──────────┘        └──────────┘
typ             └──────────┘        └──────────┘
doc             └──────────┘        └──────────┘
917  
918  theorem is_O_with.smul {k₁ k₂ : α → 𝕜} (h₁ : is_O_with c k₁ k₂ l) (h₂ : is_O_with c' f' g' l) :
id                                              └───────┘  └┘ └┘         └───────┘ └┘ └┘ └┘ 
src                                               └───────┘                  └───────┘
typ                                             └───────┘  └┘ └┘         └───────┘ └┘ └┘ └┘ 
doc                                               └───────┘                  └───────┘
919    is_O_with (c * c') (λ x, k₁ x • f' x) (λ x, k₂ x • g' x) l :=
id     └───────┘    └┘       └┘   └┘        └┘   └┘   
src    └───────┘                                      
typ    └───────┘    └┘       └┘   └┘        └┘   └┘   
doc    └───────┘
920  by refine ((h₁.norm_norm.mul h₂.norm_norm).congr rfl _ _).of_norm_norm;
id               └──────────────┘ └──────────┘        └─┘
src     └─────┘  └──────────────┘            └──────┘└─┘└────────────────┘
typ     └─────┘  └──────────────┘└──────────┘└──────┘└─┘└────────────────┘
doc     └─────┘  └──────────────┘└──────────┘└──────┘   └────────────────┘
txt     └─────┘                              └──────┘   └────────────────┘
par     └─────┘                              └──────┘   └────────────────┘
pid                                         └──────┘   └───────────────┘
st     └─────────────────────────────────────────────────────────────────────
921    by intros; simp only [norm_smul]
id                           └───────┘
src       └────┘  └─────────┘└───────┘└─
typ       └────┘  └─────────┘└───────┘└─
doc       └────┘  └─────────┘         └─
txt       └────┘  └─────────┘         └─
par       └────┘  └─────────┘         └─
pid                   └──┘└┘         
st   ───────────────────────────────────
922  
src  
typ  
doc  
txt  
par  
pid  
st   
923  theorem is_O.smul {k₁ k₂ : α → 𝕜} (h₁ : is_O k₁ k₂ l) (h₂ : is_O f' g' l) :
id                                         └──┘ └┘ └┘         └──┘ └┘ └┘ 
src                                          └──┘                └──┘
typ                                        └──┘ └┘ └┘         └──┘ └┘ └┘ 
doc                                          └──┘                └──┘
924    is_O (λ x, k₁ x • f' x) (λ x, k₂ x • g' x) l :=
id     └──┘      └┘   └┘        └┘   └┘   
src    └──┘                              
typ    └──┘      └┘   └┘        └┘   └┘   
doc    └──┘
925  by refine ((h₁.norm_norm.mul h₂.norm_norm).congr _ _).of_norm_norm;
id               └──────────────┘ └──────────┘
src     └─────┘  └──────────────┘            └───────────────────────┘
typ     └─────┘  └──────────────┘└──────────┘└───────────────────────┘
doc     └─────┘  └──────────────┘└──────────┘└───────────────────────┘
txt     └─────┘                              └───────────────────────┘
par     └─────┘                              └───────────────────────┘
pid                                         └──────────────────────┘
st     └─────────────────────────────────────────────────────────────────
926    by intros; simp only [norm_smul]
id                           └───────┘
src       └────┘  └─────────┘└───────┘└─
typ       └────┘  └─────────┘└───────┘└─
doc       └────┘  └─────────┘         └─
txt       └────┘  └─────────┘         └─
par       └────┘  └─────────┘         └─
pid                   └──┘└┘         
st   ───────────────────────────────────
927  
src  
typ  
doc  
txt  
par  
pid  
st   
928  theorem is_O.smul_is_o {k₁ k₂ : α → 𝕜} (h₁ : is_O k₁ k₂ l) (h₂ : is_o f' g' l) :
id                                              └──┘ └┘ └┘         └──┘ └┘ └┘ 
src                                               └──┘                └──┘
typ                                             └──┘ └┘ └┘         └──┘ └┘ └┘ 
doc                                               └──┘                └──┘
929    is_o (λ x, k₁ x • f' x) (λ x, k₂ x • g' x) l :=
id     └──┘      └┘   └┘        └┘   └┘   
src    └──┘                              
typ    └──┘      └┘   └┘        └┘   └┘   
doc    └──┘
930  by refine ((h₁.norm_norm.mul_is_o h₂.norm_norm).congr _ _).of_norm_norm;
id               └───────────────────┘ └──────────┘
src     └─────┘  └───────────────────┘            └───────────────────────┘
typ     └─────┘  └───────────────────┘└──────────┘└───────────────────────┘
doc     └─────┘  └───────────────────┘└──────────┘└───────────────────────┘
txt     └─────┘                                   └───────────────────────┘
par     └─────┘                                   └───────────────────────┘
pid                                              └──────────────────────┘
st     └──────────────────────────────────────────────────────────────────────
931    by intros; simp only [norm_smul]
id                           └───────┘
src       └────┘  └─────────┘└───────┘└─
typ       └────┘  └─────────┘└───────┘└─
doc       └────┘  └─────────┘         └─
txt       └────┘  └─────────┘         └─
par       └────┘  └─────────┘         └─
pid                   └──┘└┘         
st   ───────────────────────────────────
932  
src  
typ  
doc  
txt  
par  
pid  
st   
933  theorem is_o.smul_is_O {k₁ k₂ : α → 𝕜} (h₁ : is_o k₁ k₂ l) (h₂ : is_O f' g' l) :
id                                              └──┘ └┘ └┘         └──┘ └┘ └┘ 
src                                               └──┘                └──┘
typ                                             └──┘ └┘ └┘         └──┘ └┘ └┘ 
doc                                               └──┘                └──┘
934    is_o (λ x, k₁ x • f' x) (λ x, k₂ x • g' x) l :=
id     └──┘      └┘   └┘        └┘   └┘   
src    └──┘                              
typ    └──┘      └┘   └┘        └┘   └┘   
doc    └──┘
935  by refine ((h₁.norm_norm.mul_is_O h₂.norm_norm).congr _ _).of_norm_norm;
id               └───────────────────┘ └──────────┘
src     └─────┘  └───────────────────┘            └───────────────────────┘
typ     └─────┘  └───────────────────┘└──────────┘└───────────────────────┘
doc     └─────┘  └───────────────────┘└──────────┘└───────────────────────┘
txt     └─────┘                                   └───────────────────────┘
par     └─────┘                                   └───────────────────────┘
pid                                              └──────────────────────┘
st     └──────────────────────────────────────────────────────────────────────
936    by intros; simp only [norm_smul]
id                           └───────┘
src       └────┘  └─────────┘└───────┘└─
typ       └────┘  └─────────┘└───────┘└─
doc       └────┘  └─────────┘         └─
txt       └────┘  └─────────┘         └─
par       └────┘  └─────────┘         └─
pid                   └──┘└┘         
st   ───────────────────────────────────
937  
src  
typ  
doc  
txt  
par  
pid  
st   
938  theorem is_o.smul {k₁ k₂ : α → 𝕜} (h₁ : is_o k₁ k₂ l) (h₂ : is_o f' g' l) :
id                                         └──┘ └┘ └┘         └──┘ └┘ └┘ 
src                                          └──┘                └──┘
typ                                        └──┘ └┘ └┘         └──┘ └┘ └┘ 
doc                                          └──┘                └──┘
939    is_o (λ x, k₁ x • f' x) (λ x, k₂ x • g' x) l :=
id     └──┘      └┘   └┘        └┘   └┘   
src    └──┘                              
typ    └──┘      └┘   └┘        └┘   └┘   
doc    └──┘
940  by refine ((h₁.norm_norm.mul h₂.norm_norm).congr _ _).of_norm_norm;
id               └──────────────┘ └──────────┘
src     └─────┘  └──────────────┘            └───────────────────────┘
typ     └─────┘  └──────────────┘└──────────┘└───────────────────────┘
doc     └─────┘  └──────────────┘└──────────┘└───────────────────────┘
txt     └─────┘                              └───────────────────────┘
par     └─────┘                              └───────────────────────┘
pid                                         └──────────────────────┘
st     └─────────────────────────────────────────────────────────────────
941    by intros; simp only [norm_smul]
id                           └───────┘
src       └────┘  └─────────┘└───────┘└─
typ       └────┘  └─────────┘└───────┘└─
doc       └────┘  └─────────┘         └─
txt       └────┘  └─────────┘         └─
par       └────┘  └─────────┘         └─
pid                   └──┘└┘         
st   ───────────────────────────────────
942  
src  
typ  
doc  
txt  
par  
pid  
st   
943  end smul
944  
945  /-! ### Relation between `f = o(g)` and `f / g → 0` -/
946  
947  theorem is_o.tendsto_0 {f g : α → 𝕜} {l : filter α} (h : is_o f g l) :
id                                           └────┘        └──┘   
src                                            └────┘         └──┘
typ                                          └────┘        └──┘   
doc                                                           └──┘
948    tendsto (λ x, f x / (g x)) l (𝓝 0) :=
id     └─────┘                
src    └─────┘                      
typ    └─────┘                
doc    └─────┘                       
949  have eq₁ : is_o (λ x, f x / g x) (λ x, g x / g x) l,
id              └──┘                       
src             └──┘                           
typ             └──┘                       
doc             └──┘
950    from h.mul_is_O (is_O_refl _ _),
id          └───────┘  └───────┘
src          └───────┘  └───────┘
typ         └───────┘  └───────┘
951  have eq₂ : is_O (λ x, g x / g x) (λ x, (1 : 𝕜)) l,
id              └──┘                         
src             └──┘           
typ             └──┘                         
doc             └──┘
952    from is_O_of_le _ (λ x, by by_cases h : ∥g x∥ = 0; simp [h, zero_le_one]),
id          └────────┘                                      └─────────┘
src         └────────┘            └───────┘ └─┘  └┘  └────┘ └┘└─────────┘
typ         └────────┘           └───────┘ └─┘└┘  └────┘└┘└─────────┘
doc                               └───────┘ └─┘     └┘  └────┘ └┘           
txt                               └───────┘ └─┘     └┘  └────┘ └┘           
par                               └───────┘ └─┘     └┘  └────┘ └┘           
pid                                        └─┘            └┘           
st                               └────────────────────────────────────────────┘
953  (is_o_one_iff 𝕜).mp (eq₁.trans_is_O eq₂)
id    └──────────┘  └┘   └─┘└─────────┘ └─┘
src   └──────────┘   └┘      └─────────┘
typ   └──────────┘  └┘   └─┘└─────────┘ └─┘
954  
955  private theorem is_o_of_tendsto {f g : α → 𝕜} {l : filter α}
id                                                    └────┘ 
src                                                     └────┘
typ                                                   └────┘ 
956      (hgf : ∀ x, g x = 0 → f x = 0) (h : tendsto (λ x, f x / (g x)) l (𝓝 0)) :
id                                    └─────┘                
src                                        └─────┘                      
typ                                   └─────┘                
doc                                          └─────┘                       
957    is_o f g l :=
id     └──┘   
src    └──┘
typ    └──┘   
doc    └──┘
958  have eq₁ : is_o (λ x, f x / (g x)) (λ x, (1 : 𝕜)) l,
id              └──┘                           
src             └──┘           
typ             └──┘                           
doc             └──┘
959    from (is_o_one_iff _).mpr h,
id           └──────────┘   └─┘  
src          └──────────┘   └─┘
typ          └──────────┘   └─┘  
960  have eq₂ : is_o (λ x, f x / g x * g x) g l,
id              └──┘                
src             └──┘                
typ             └──┘                
doc             └──┘
961    by convert eq₁.mul_is_O (is_O_refl _ _); simp,
id                └──────────┘  └───────┘
src       └──────┘└──────────┘ └───────┘└───┘  └──┘
typ       └──────┘└──────────┘ └───────┘└───┘  └──┘
doc       └──────┘                      └───┘  └──┘
txt       └──────┘                      └───┘  └──┘
par       └──────┘                      └───┘  └──┘
pid                                    └───┘
st       └─────────────────────────────────────────┘
962  have eq₃ : is_O f (λ x, f x / g x * g x) l,
id              └──┘                
src             └──┘                  
typ             └──┘                
doc             └──┘
963    begin
st     └─────
964      refine is_O_of_le _ (λ x, _),
id              └────────┘
src      └─────┘└────────┘└─┘  └────┘
typ      └─────┘└────────┘└─┘  └────┘
doc      └─────┘          └─┘  └────┘
txt      └─────┘          └─┘  └────┘
par      └─────┘          └─┘  └────┘
pid                      └─┘  └────┘
st   ───────────────────────────────┘└─
965      by_cases H : g x = 0,
id                      
src      └───────┘ └─┘  └┘
typ      └───────┘ └─┘└┘
doc      └───────┘ └─┘   └┘
txt      └───────┘ └─┘   └┘
par      └───────┘ └─┘   └┘
pid               └─┘   
st   ───────────────────────┘└─
966      { simp only [H, hgf _ H, mul_zero] },
id                      └─┘     └──────┘
src        └─────────┘ └┘   └─┘ └┘└──────┘└┘
typ        └─────────┘└┘└─┘└─┘└┘└──────┘└┘
doc        └─────────┘ └┘   └─┘ └┘        └┘
txt        └─────────┘ └┘   └─┘ └┘        └┘
par        └─────────┘ └┘   └─┘ └┘        └┘
pid            └──┘└┘ └┘   └─┘ └┘        
st   ─────┘└───────────────────────────────┘└┘
967      { simp only [div_mul_cancel _ H] }
id                    └────────────┘   
src        └─────────┘└────────────┘└─┘ └┘
typ        └─────────┘└────────────┘└─┘└┘
doc        └─────────┘              └─┘ └┘
txt        └─────────┘              └─┘ └┘
par        └─────────┘              └─┘ └┘
pid            └──┘└┘              └─┘ 
st   ────────────────────────────────────┘└─
968    end,
st   ────┘
969  eq₃.trans_is_o eq₂
id   └─┘└─────────┘ └─┘
src     └─────────┘
typ  └─┘└─────────┘ └─┘
970  
971  theorem is_o_iff_tendsto {f g : α → 𝕜} {l : filter α}
id                                             └────┘ 
src                                              └────┘
typ                                            └────┘ 
972      (hgf : ∀ x, g x = 0 → f x = 0) :
id                           
src                               
typ                          
973    is_o f g l ↔ tendsto (λ x, f x / (g x)) l (𝓝 0) :=
id     └──┘     └─────┘                
src    └──┘        └─────┘                      
typ    └──┘     └─────┘                
doc    └──┘         └─────┘                       
974  iff.intro is_o.tendsto_0 (is_o_of_tendsto hgf)
id   └───────┘ └────────────┘  └─────────────┘ └─┘
src  └───────┘ └────────────┘  └─────────────┘
typ  └───────┘ └────────────┘  └─────────────┘ └─┘
975  
976  /-! ### Miscellanous lemmas -/
977  
978  theorem is_o_pow_pow {m n : ℕ} (h : m < n) :
id                                        
src                                       
typ                                       
979    is_o (λ(x : 𝕜), x^n) (λx, x^m) (𝓝 0) :=
id     └──┘                    
src    └──┘                          
typ    └──┘                    
doc    └──┘                            
980  begin
st   └─────
981    let p := n - m,
id                
src    └───────┘ 
typ    └───────┘
doc    └───────┘  
txt    └───────┘  
par    └───────┘  
pid    └───┘└─┘  
st   ───────────────┘└─
982    have nmp : n = m + p := (nat.add_sub_cancel' (le_of_lt h)).symm,
id                         └─────────────────┘  └──────┘ 
src    └─────────┘   └──┘ └─────────────────┘ └──────┘ └─────┘
typ    └─────────┘└──┘ └─────────────────┘ └──────┘└─────┘
doc    └─────────┘     └──┘                              └─────┘
txt    └─────────┘     └──┘                              └─────┘
par    └─────────┘     └──┘                              └─────┘
pid    └──────┘└─┘     └──┘                              └────┘
st   ────────────────────────────────────────────────────────────────┘└─
983    have : (λ(x : 𝕜), x^m) = (λx, x^m * 1), by simp only [mul_one],
id                                                       └─────┘
src    └─────┘  └───┘ └─┘  └┘   └─┘   └─┘     └─────────┘└─────┘
typ    └─────┘  └───┘└─┘  └┘   └─┘  └─┘     └─────────┘└─────┘
doc    └─────┘  └───┘ └─┘   └┘   └─┘    └─┘     └─────────┘       
txt    └─────┘  └───┘ └─┘   └┘   └─┘    └─┘     └─────────┘       
par    └─────┘  └───┘ └─┘   └┘   └─┘    └─┘     └─────────┘       
pid    └───┘└┘  └───┘ └─┘   └┘   └─┘    └─┘         └──┘└┘       
st   ───────────────────────────────────────┘                        └─
984    simp only [this, pow_add, nmp],
id                └──┘  └─────┘  └─┘
src    └─────────┘    └┘└─────┘└┘   
typ    └─────────┘└──┘└┘└─────┘└┘└─┘
doc    └─────────┘    └┘       └┘   
txt    └─────────┘    └┘       └┘   
par    └─────────┘    └┘       └┘   
pid        └──┘└┘    └┘       └┘   
st   ───────────────────────────────┘└─
985    refine is_O.mul_is_o (is_O_refl _ _) ((is_o_one_iff _).2 _),
id            └───────────┘  └───────┘        └──────────┘
src    └─────┘└───────────┘ └───────┘└────┘  └──────────┘└──────┘
typ    └─────┘└───────────┘ └───────┘└────┘  └──────────┘└──────┘
doc    └─────┘                       └────┘              └──────┘
txt    └─────┘                       └────┘              └──────┘
par    └─────┘                       └────┘              └──────┘
pid                                 └────┘              └──────┘
st   ────────────────────────────────────────────────────────────┘└─
986    convert (continuous_pow p).tendsto (0 : 𝕜),
id              └────────────┘                
src    └──────┘ └────────────┘ └────────┘ └──┘ 
typ    └──────┘ └────────────┘└────────┘ └──┘
doc    └──────┘                └────────┘ └──┘ 
txt    └──────┘                └────────┘ └──┘ 
par    └──────┘                └────────┘ └──┘ 
pid                           └────────┘ └──┘ 
st   ───────────────────────────────────────────┘└─
987    exact (zero_pow (nat.sub_pos_of_lt h)).symm
id            └──────┘  └───────────────┘ 
src    └────┘ └──────┘ └───────────────┘ └──────┘
typ    └────┘ └──────┘ └───────────────┘└──────┘
doc    └────┘                            └──────┘
txt    └────┘                            └──────┘
par    └────┘                            └──────┘
pid                                     └────┘└┘
st   ─────────────────────────────────────────────┘
988  end
st   └─┘
989  
990  theorem is_o_pow_id {n : ℕ} (h : 1 < n) :
id                                      
src                                    
typ                                     
991    is_o (λ(x : 𝕜), x^n) (λx, x) (𝓝 0) :=
id     └──┘                    
src    └──┘                         
typ    └──┘                    
doc    └──┘                          
992  by { convert is_o_pow_pow h, simp only [pow_one] }
id                └──────────┘              └─────┘
src       └──────┘└──────────┘   └─────────┘└─────┘└┘
typ       └──────┘└──────────┘  └─────────┘└─────┘└┘
doc       └──────┘               └─────────┘       └┘
txt       └──────┘               └─────────┘       └┘
par       └──────┘               └─────────┘       └┘
pid                                 └──┘└┘       
st     └───────────────────────┘└────────────────────┘└┘
993  
994  theorem is_O_with.right_le_sub_of_lt_1 {f₁ f₂ : α → E'} (h : is_O_with c f₁ f₂ l) (hc : c < 1) :
id                                                      └┘       └───────┘  └┘ └┘          
src                                                               └───────┘                    
typ                                                     └┘       └───────┘  └┘ └┘          
doc                                                               └───────┘
995    is_O_with (1 / (1 - c)) f₂ (λx, f₂ x - f₁ x) l :=
id     └───────┘            └┘     └┘   └┘   
src    └───────┘                          
typ    └───────┘            └┘     └┘   └┘   
doc    └───────┘
996  mem_sets_of_superset h $ λ x hx,
id   └──────────────────┘       └┘
src  └──────────────────┘
typ  └──────────────────┘       └┘
997  begin
st   └─────
998    simp only [mem_set_of_eq] at hx ⊢,
id                └───────────┘
src    └─────────┘└───────────┘└───────┘
typ    └─────────┘└───────────┘└───────┘
doc    └─────────┘             └───────┘
txt    └─────────┘             └───────┘
par    └─────────┘             └───────┘
pid        └──┘└┘             └─────┘
st   ──────────────────────────────────┘└─
999    rw [mul_comm, one_div_eq_inv, ← div_eq_mul_inv, le_div_iff, mul_sub, mul_one, mul_comm],
id         └──────┘  └────────────┘    └────────────┘  └────────┘  └─────┘  └─────┘  └──────┘
src    └──┘└──────┘└┘└────────────┘└──┘└────────────┘└┘└────────┘└┘└─────┘└┘└─────┘└┘└──────┘
typ    └──┘└──────┘└┘└────────────┘└──┘└────────────┘└┘└────────┘└┘└─────┘└┘└─────┘└┘└──────┘
doc    └──┘        └┘              └──┘              └┘          └┘       └┘       └┘        
txt    └──┘        └┘              └──┘              └┘          └┘       └┘       └┘        
par    └──┘        └┘              └──┘              └┘          └┘       └┘       └┘        
pid      └┘        └┘              └──┘              └┘          └┘       └┘       └┘        
st   ─────────────┘└──────────────┘└────────────────┘└──────────┘└───────┘└───────┘└────────┘└──
1000    { exact le_trans (sub_le_sub_left hx _) (norm_sub_norm_le _ _) },
id             └──────┘  └─────────────┘ └┘     └──────────────┘
src      └────┘└──────┘ └─────────────┘  └──┘ └──────────────┘└────┘
typ      └────┘└──────┘ └─────────────┘└┘└──┘ └──────────────┘└────┘
doc      └────┘                          └──┘                 └────┘
txt      └────┘                          └──┘                 └────┘
par      └────┘                          └──┘                 └────┘
pid                                     └──┘                 └───┘
st   ───┘└───────────────────────────────────────────────────────────┘└┘
1001    { exact sub_pos.2 hc }
id             └─────┘   └┘
src      └────┘└─────┘└─┘  
typ      └────┘└─────┘└─┘└┘
doc      └────┘       └─┘  
txt      └────┘       └─┘  
par      └────┘       └─┘  
pid                  └─┘  
st   ──────────────────────┘└─
1002  end
st   ──┘
1003  
1004  theorem is_O_with.right_le_add_of_lt_1 {f₁ f₂ : α → E'} (h : is_O_with c f₁ f₂ l) (hc : c < 1) :
id                                                      └┘       └───────┘  └┘ └┘          
src                                                               └───────┘                    
typ                                                     └┘       └───────┘  └┘ └┘          
doc                                                               └───────┘
1005    is_O_with (1 / (1 - c)) f₂ (λx, f₁ x + f₂ x) l :=
id     └───────┘            └┘     └┘   └┘   
src    └───────┘                          
typ    └───────┘            └┘     └┘   └┘   
doc    └───────┘
1006  (h.neg_right.right_le_sub_of_lt_1 hc).neg_right.neg_left.congr rfl (λ x, neg_neg _)
id    └────────┘└───────────────────┘ └┘ └───────┘ └──────┘ └───┘  └─┘      └─────┘
src              └───────────────────┘                       └───┘  └─┘       └─────┘
typ   └────────┘└───────────────────┘ └┘ └───────┘ └──────┘ └───┘  └─┘      └─────┘
doc    └────────┘                         └───────┘ └──────┘
1007    (λ x, by rw [neg_sub, sub_neg_eq_add])
id                 └─────┘  └────────────┘
src             └──┘└─────┘└┘└────────────┘
typ            └──┘└─────┘└┘└────────────┘
doc             └──┘       └┘              
txt             └──┘       └┘              
par             └──┘       └┘              
pid               └┘       └┘              
st             └──────────┘└──────────────┘
1008  
1009  end asymptotics